From dc034c2b09fec19599f1344946a715c33e502af4 Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Sun, 11 Jun 2023 12:33:18 +0000
Subject: [PATCH] added preliminary def of krullDimGE

---
 comm_alg/grant.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean
index de3e50f..92b1716 100644
--- a/comm_alg/grant.lean
+++ b/comm_alg/grant.lean
@@ -36,4 +36,7 @@ lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop 
     
     sorry
   -- norm_cast
-  sorry
\ No newline at end of file
+  sorry
+
+def krullDimGE (R : Type _) [CommRing R] (n : ℕ) :=
+  ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1
\ No newline at end of file