From d0071924df883d186c0b805e6b9007656d9f36f5 Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Sat, 10 Jun 2023 21:04:25 -0700
Subject: [PATCH 1/5] add stuff

---
 .DS_Store | Bin 0 -> 6148 bytes
 1 file changed, 0 insertions(+), 0 deletions(-)
 create mode 100644 .DS_Store

diff --git a/.DS_Store b/.DS_Store
new file mode 100644
index 0000000000000000000000000000000000000000..6d98085373769dd4c6eebf58c63f4db066814689
GIT binary patch
literal 6148
zcmeHKyH3ME5S%3`EYYM)dB4CPoTBgrd_V$;L}TOv(YxZi_%vo81(Bf(O*Cum&E4M4
zS)St73&3_C=LcW|V4yqV(}$(`zWc)NDq=)B&p6;2BVNz%r*V<}d%(E^PMGk<=Li2~
znnvH0NdYM!1*Cu!kOEg#pvvoTf7MfUm=ur#x1fOE4~_2F3+KeRIygiNKwL8%#(DG-
z#O48FFPsw@p;=OiNwsP*Ea{B5%Ik%5V$xyNd|18Nszb4OJI`;C4(o{;rGON;RA80M
zjo1H2`XBxOB}pqOAO&tp0bB2%_B(!3)z-zwd97{qBi(bp=x&?`g+r8MVw7Vpyc};M
cDf61ox!()t#Go@CbfSI+To;)X_-_Ti0jAm&VE_OC

literal 0
HcmV?d00001


From 29ed7e50387e618af32faebe3bd5bc2bf08cbd7d Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Sat, 10 Jun 2023 21:10:01 -0700
Subject: [PATCH 2/5] test

---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitignore b/.gitignore
index 20c60d7..e254e15 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,3 @@
 /build
 /lake-packages/*
+.DS_Store
\ No newline at end of file

From 53ce99993ecf4436abfb4b89cec26e068dd846f2 Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Sat, 10 Jun 2023 21:10:36 -0700
Subject: [PATCH 3/5] test

---
 test.md | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 test.md

diff --git a/test.md b/test.md
new file mode 100644
index 0000000..af2a4c4
--- /dev/null
+++ b/test.md
@@ -0,0 +1 @@
+Just checking out
\ No newline at end of file

From 8c0b286765ec910ae7c25acd2149043ab464f8ce Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Sat, 10 Jun 2023 21:26:45 -0700
Subject: [PATCH 4/5] delete test

---
 test.md | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 test.md

diff --git a/test.md b/test.md
deleted file mode 100644
index af2a4c4..0000000
--- a/test.md
+++ /dev/null
@@ -1 +0,0 @@
-Just checking out
\ No newline at end of file

From 16b933aeacf3aac0585695505e8c44a501863127 Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Sun, 11 Jun 2023 21:41:21 -0700
Subject: [PATCH 5/5] 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
+
+
+
+
+
+