diff --git a/comm_alg/krull.lean b/comm_alg/krull.lean
index 2a5af42..1067e63 100644
--- a/comm_alg/krull.lean
+++ b/comm_alg/krull.lean
@@ -41,4 +41,4 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
 lemma height_eq_dim_localization [Ideal.IsPrime I] :
   height I = krull_dim (Localization.AtPrime I) := sorry
 
-lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I) ≤ krull_dim R := sorry
\ No newline at end of file
+lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I) ≤ krull_dim R := sorry