From 16b933aeacf3aac0585695505e8c44a501863127 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Sun, 11 Jun 2023 21:41:21 -0700 Subject: [PATCH] just the statement --- comm_alg/jayden(krull-dim-zero).lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 comm_alg/jayden(krull-dim-zero).lean 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 + + + + + +