diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index 1bd2829..228f0b1 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -1,4 +1,5 @@
-import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.RingTheory.FiniteType
 import Mathlib.Order.Height
 import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.RingTheory.DedekindDomain.Basic
@@ -33,11 +34,12 @@ noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.c
 
 lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) :
   iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) ≤ n ↔
-  ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := by
-    convert @iSup_le_iff (WithBot ℕ∞) (PrimeSpectrum R) inferInstance _ (↑n)
+  ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
 
 --some propositions that would be nice to be able to eventually
 
+lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := sorry
+
 lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry
 
 #check Ring.DimensionLEOne
diff --git a/CommAlg/resources.lean b/CommAlg/resources.lean
index bb30ae3..2d5d227 100644
--- a/CommAlg/resources.lean
+++ b/CommAlg/resources.lean
@@ -7,6 +7,7 @@ useful lemmas and definitions
 import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.RingTheory.Noetherian
 import Mathlib.RingTheory.Artinian
+import Mathlib.RingTheory.FiniteType
 import Mathlib.Order.Height
 import Mathlib.RingTheory.MvPolynomial.Basic
 import Mathlib.RingTheory.Ideal.Over
@@ -59,6 +60,11 @@ variable (I : Ideal R)
 --Theorems relating primes of a ring to primes of a quotient
 #check PrimeSpectrum.range_comap_of_surjective
 
+--There's a lot of theorems about finite-type algebras
+#check Algebra.FiniteType.polynomial
+#check Algebra.FiniteType.mvPolynomial
+#check Algebra.FiniteType.of_surjective
+
 -- There is a notion of short exact sequences but the number of theorems are lacking
 -- For example, I couldn't find anything saying that for a ses 0 -> A -> B -> C -> 0
 -- of R-modules, A and C being FG implies that B is FG