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