height_le_ringKrullDim_of_ne_top — Mathlib

English

If I ≠ ⊤, then I.height ≤ ringKrullDim R.

Русский

Если I ≠ ⊤, то height(I) ≤ ringKrullDim R.

LaTeX

$$I ≠ ⊤ → I.height ≤ \mathrm{ringKrullDim}(R)$$

Lean4

theorem height_le_ringKrullDim_of_ne_top {I : Ideal R} (h : I ≠ ⊤) : I.height ≤ ringKrullDim R :=
  by
  rw [Ideal.height]
  obtain ⟨P, hP⟩ : Nonempty (I.minimalPrimes) := Ideal.nonempty_minimalPrimes h
  have := Ideal.minimalPrimes_isPrime hP
  refine le_trans ?_ (Ideal.primeHeight_le_ringKrullDim (I := P))
  simpa using iInf₂_le _ hP

Похожие утверждения