diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean
index bb30ae3..2d5d227 100644
--- a/comm_alg/resources.lean
+++ b/comm_alg/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