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