krullDim_eq_of_orderIso — Mathlib

English

If f is an order isomorphism, heights are preserved, hence Krull dimension is preserved.

Русский

Если f — изоморфизм порядка, высоты сохраняются, значит и размерность сохраняется.

LaTeX

$$\operatorname{krullDim}(\alpha) = \operatorname{krullDim}(\beta) \text{ in presence of an isomorphism } f$$

Lean4

theorem krullDim_eq_of_orderIso (f : α ≃o β) : krullDim α = krullDim β :=
  le_antisymm (krullDim_le_of_strictMono _ f.strictMono) <| krullDim_le_of_strictMono _ f.symm.strictMono

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