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