From e22b18e7c5964baf74ee825a0144a0b10379657c Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Mon, 12 Jun 2023 20:57:49 +0000 Subject: [PATCH] TESTMOna --- comm_alg/krull.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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