SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 23:48:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

Defining lemmas

Browse source
This commit is contained in:
Sameer Savkar 2023-06-12 13:34:09 -07:00
parent 8e7ddca721
commit cbb0c6ce7a
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
comm_alg/sameer(artinian-rings).lean
View file

@ -4,8 +4,12 @@ import Mathlib.RingTheory.Artinian
import Mathlib.RingTheory.Ideal.Quotient import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic 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 -- Use Stacks project proof since it's broken into lemmas