krullDim_eq_iSup_length — Mathlib

English

If α is finite-dimensional, then Krull dimension equals the length of the longest chain.

Русский

Если α конечно размерен, то размерность Крулла равна длине самой длинной цепи.

LaTeX

$$\operatorname{krullDim}(\alpha) = (\mathrm{LTSeries.longestOf}(\alpha)).length$$

Lean4

/-- A definition of krullDim for nonempty `α` that avoids `WithBot` -/
theorem krullDim_eq_iSup_length [Nonempty α] : krullDim α = ⨆ (p : LTSeries α), (p.length : ℕ∞) :=
  by
  unfold krullDim
  rw [WithBot.coe_iSup (OrderTop.bddAbove _)]
  rfl

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