SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 07:38:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

added more sorried statements

Browse source
This commit is contained in:
leopoldmayer 2023-06-14 12:02:01 -07:00
parent 2737f8bba6
commit ebbbfc88c3
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
CommAlg/krull.lean
View file

@ -226,7 +226,11 @@ lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
krullDim R + 1 = krullDim (Polynomial R) := sorry 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 : lemma height_eq_dim_localization :
height I = krullDim (Localization.AtPrime I.asIdeal) := sorry 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 lemma height_add_dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry