diff --git a/.gitignore b/.gitignore index e254e15..c666579 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ /build /lake-packages/* -.DS_Store \ No newline at end of file +.DS_Store +.cache/ \ No newline at end of file diff --git a/comm_alg/sameer(artinian-rings).lean b/comm_alg/sameer(artinian-rings).lean new file mode 100644 index 0000000..aae0fd7 --- /dev/null +++ b/comm_alg/sameer(artinian-rings).lean @@ -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