instLocallyFiniteOrderUnitsWithZero

English

If X isLocallyFiniteOrdered and has a group structure with zero, then its units with zero inherit a locally finite order.

Русский

Единицы WithZero(X) наследуют локально конечный порядок от структуры X.

LaTeX

$$$\text{LocallyFiniteOrder}((\mathrm{Units}(\mathrm{WithZero}(X))))$$$

Lean4

instance [Group X] : LocallyFiniteOrder (WithZero X)ˣ :=
  OrderIso.locallyFiniteOrder (OrderMonoidIso.unitsWithZero (α := X) : (WithZero X)ˣ ≃o X)

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