English
If α ≃o β, then krullDim α = krullDim β.
Русский
Если α эквивалентно β как порядок, размерности Крулла совпадают.
LaTeX
$$\operatorname{krullDim}(\alpha) = \operatorname{krullDim}(\beta) \text{ if } \alpha \cong_o \beta$$
Lean4
/-- The Krull dimension is the supremum of the elements' heights.
If `α` is `Nonempty`, then `krullDim_eq_iSup_height_of_nonempty`, with the coercion from
`ℕ∞` to `WithBot ℕ∞` outside the supremum, can be more convenient.
-/
theorem krullDim_eq_iSup_height : krullDim α = ⨆ (a : α), ↑(height a) := by
cases isEmpty_or_nonempty α with
| inl h => rw [krullDim_eq_bot, ciSup_of_empty]
| inr h => rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]