From ebbbfc88c32e21ca47be4e9aa3067c8a9f5005ad Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Wed, 14 Jun 2023 12:02:01 -0700 Subject: [PATCH] added more sorried statements --- CommAlg/krull.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 06e6d0d..59fd048 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