diff --git a/.DS_Store b/.DS_Store new file mode 100644 index 0000000..6d98085 Binary files /dev/null and b/.DS_Store differ diff --git a/comm_alg/jayden(krull-dim-zero).lean b/comm_alg/jayden(krull-dim-zero).lean new file mode 100644 index 0000000..0e9b32f --- /dev/null +++ b/comm_alg/jayden(krull-dim-zero).lean @@ -0,0 +1,15 @@ +import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Artinian +import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic + +lemma dim_zero_Noetherian_is_Artinian (R : Type _) (IsNoetherianRing R) (krull_dim R = 0) : IsArtinianRing R := by sorry + +-- Use Stacks project proof since it's broken into lemmas + + + + + +