From 46908891497cd2510c470a563e127b48843a2b76 Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Wed, 14 Jun 2023 21:35:36 +0000
Subject: [PATCH] proved dim_eq_zero_iff

---
 CommAlg/krull.lean | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index d58a065..b2d0230 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -169,11 +169,16 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal
     exact hc2
 
 lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
-  constructor <;> intro h
-  . intro I
-    sorry
-  . sorry
-  
+  rw [←dim_le_zero_iff]
+  obtain ⟨n, hn⟩ := krullDim_nonneg_of_nontrivial R
+  have : n ≥ 0 := zero_le n
+  change _ ≤ _ at this
+  rw [←WithBot.coe_le_coe,←hn] at this
+  change (0 : WithBot ℕ∞) ≤ _ at this
+  constructor <;> intro h'
+  rw [h']
+  exact le_antisymm h' this
+
 @[simp]
 lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by
       constructor