diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean
index 80e5d39..86c05fc 100644
--- a/comm_alg/grant.lean
+++ b/comm_alg/grant.lean
@@ -1,6 +1,12 @@
-import Mathlib.Analysis.Seminorm
+import Mathlib.Order.KrullDimension
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 
 def hello : IO Unit := do
   IO.println "Hello, World!"
 
-#eval hello
\ No newline at end of file
+#eval hello
+
+#check (p q : PrimeSpectrum _) → (p ≤ q)
+#check Preorder (PrimeSpectrum _)
+
+#check krullDim (PrimeSpectrum _)
\ No newline at end of file