SinTan1729
/
comm_alg
mirror of https://github.com/GTBarkley/comm_alg.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

removed sorried lemmas that are now proved elsewhe

This commit is contained in:
leopoldmayer 2023-06-16 14:54:36 -07:00
parent d896e75633
commit 4c17c4c903
1 changed files with 0 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
CommAlg/krull.lean
View File

@ -442,8 +442,6 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD
have : {J | J < P}.Nonempty := Set.nonempty_of_mem this
rwa [←Set.one_le_chainHeight_iff, ←WithBot.one_le_coe] at this
lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
krullDim R + 1 ≤ krullDim (Polynomial R) := sorry
-- lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
-- krullDim R + 1 = krullDim (Polynomial R) := sorry
@ -457,6 +455,4 @@ lemma dim_mvPolynomial [Field K] (n : ℕ) : krullDim (MvPolynomial (Fin n) K) =
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