Some changes to dim_eq_dim_poly_add_one

This commit is contained in:
Sayantan Santra 2023-06-15 19:36:02 -07:00
parent e9fbb1a521
commit eb1e6118a0
Signed by: SinTan1729
GPG key ID: EB3E68BFBA25C85F

View file

@ -16,7 +16,8 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD
-- unfold krullDim
rw [le_antisymm_iff]
constructor
· sorry
·
sorry
· suffices : ∃I : PrimeSpectrum (Polynomial K), 1 ≤ (height I : WithBot ℕ∞)
· obtain ⟨I, h⟩ := this
have : (height I : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum (Polynomial K)), ↑(height I) := by