From 868f098749083d5c870f5e98af8b5205fbdadb90 Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Sun, 11 Jun 2023 00:36:27 +0000
Subject: [PATCH] checked preliminary definition of Krull dimension

---
 comm_alg/grant.lean | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

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