created a new file
This commit is contained in:
parent
3fac57ad02
commit
8e7ddca721
|
@ -1,3 +1,4 @@
|
||||||
/build
|
/build
|
||||||
/lake-packages/*
|
/lake-packages/*
|
||||||
.DS_Store
|
.DS_Store
|
||||||
|
.cache/
|
|
@ -0,0 +1,11 @@
|
||||||
|
import Mathlib.RingTheory.Ideal.Basic
|
||||||
|
import Mathlib.RingTheory.Noetherian
|
||||||
|
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 IsPrimeisMaximal (R : Type_) (isArtinianRing R) (Ideal I) : IsPrimeisMaximal R := by sorry
|
||||||
|
|
||||||
|
-- Use Stacks project proof since it's broken into lemmas
|
Loading…
Reference in New Issue