From d30702fb10a79ca854f1feb58037082377e0529a Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Wed, 14 Jun 2023 03:45:23 +0000 Subject: [PATCH] updated def --- .docker/test.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.docker/test.lean b/.docker/test.lean index a851192..888270c 100644 --- a/.docker/test.lean +++ b/.docker/test.lean @@ -88,10 +88,11 @@ instance tada3 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGr letI := Module.compHom (⨁ j, 𝓜 j) (ofZeroRingHom 𝒜) exact Dfinsupp.single_injective.module (𝒜 0) (of 𝓜 i) (mylem 𝒜 𝓜 i) + -- (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) + noncomputable def hilbert_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] - [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) - : ℤ → ℕ∞ := fun i => (length (𝒜 0) (𝓜 i)) + [DirectSum.Gmodule 𝒜 𝓜] (hilb : ℤ → ℕ∞) := ∀ i, hilb i = (length (𝒜 0) (𝓜 i)) lemma hilbertz (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜]