diff --git a/comm_alg/jayden(krull-dim-zero).lean b/comm_alg/jayden(krull-dim-zero).lean
index 0e9b32f..7be91c5 100644
--- a/comm_alg/jayden(krull-dim-zero).lean
+++ b/comm_alg/jayden(krull-dim-zero).lean
@@ -1,12 +1,25 @@
 import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.RingTheory.Noetherian
+import Mathlib.Order.KrullDimension
 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
+variable {R : Type _} [CommRing R]
 
--- Use Stacks project proof since it's broken into lemmas
+-- Repeats the definition by Monalisa
+noncomputable def length : krullDim (Submodule _ _)
+
+
+-- The following is Stacks Lemma 10.60.5
+lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : 
+    IsNoetherianRing R ∧ krull_dim R = 0 ↔ IsArtinianRing R := by 
+  sorry
+
+#check IsNoetherianRing
+
+-- The following is Stacks Lemma 10.53.6
+lemma IsArtinian_iff_finite_length : IsArtinianRing R ↔ ∃ n : ℕ, length R R ≤ n := by sorry