diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index ec94d36..2111469 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -226,7 +226,11 @@ lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
 lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
   krullDim R + 1 = krullDim (Polynomial R) := sorry
 
+lemma dim_mvPolynomial [Field K] (n : ℕ) : krullDim (MvPolynomial (Fin n) K) = n := sorry
+
 lemma height_eq_dim_localization :
   height I = krullDim (Localization.AtPrime I.asIdeal) := sorry
 
+lemma dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry
+
 lemma height_add_dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry
\ No newline at end of file