From cbb0c6ce7af913b76cccb7462528aa8d071cc0c5 Mon Sep 17 00:00:00 2001 From: Sameer Savkar Date: Mon, 12 Jun 2023 13:34:09 -0700 Subject: [PATCH] Defining lemmas --- comm_alg/sameer(artinian-rings).lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/comm_alg/sameer(artinian-rings).lean b/comm_alg/sameer(artinian-rings).lean index aae0fd7..381680b 100644 --- a/comm_alg/sameer(artinian-rings).lean +++ b/comm_alg/sameer(artinian-rings).lean @@ -4,8 +4,12 @@ import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Ideal.Quotient import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic -lemma quotientRing_is_Artinian (R : Type _) (isArtinianRing R) (Ideal I) : IsArtinianRing R := by sorry +lemma quotientRing_is_Artinian (R : Type _) [CommRing R] (I : Ideal R) (IsArt : IsArtinianRing R): +IsArtinianRing (R⧸I) := by sorry + +#check Ideal.IsPrime + +lemma IsPrimeMaximal (R : Type _) [CommRing R] (I : Ideal R) (IsArt : IsArtinianRing R) (isPrime : Ideal.IsPrime I) : Ideal.IsMaximal I := by sorry -lemma IsPrimeisMaximal (R : Type_) (isArtinianRing R) (Ideal I) : IsPrimeisMaximal R := by sorry -- Use Stacks project proof since it's broken into lemmas