From 5f241e80f164fb255953686d33c21d4a12cd1df1 Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Tue, 13 Jun 2023 14:16:53 -0700
Subject: [PATCH] Added a comment

---
 CommAlg/krull.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index c021d74..e8941a3 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -88,7 +88,7 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
   . rw [h.forall_iff]
     trivial
 
-lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry
+lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry -- It's been done in another file
 
 #check Ring.DimensionLEOne
 lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry