SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-10-16 19:43:55 -05:00
Code Issues Projects Releases Packages Wiki Activity

TESTMOna

Browse source
This commit is contained in:
monula95 dutta 2023-06-12 20:57:49 +00:00
parent d1c10a2d3a
commit e22b18e7c5
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
comm_alg/krull.lean
View file

@ -41,4 +41,4 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
lemma height_eq_dim_localization [Ideal.IsPrime I] : lemma height_eq_dim_localization [Ideal.IsPrime I] :
height I = krull_dim (Localization.AtPrime I) := sorry 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 lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I) ≤ krull_dim R := sorry