withZeroUnits — Mathlib

English

The order isomorphism between units and the base group with zero.

Русский

Изоморфизм порядка между модулями единиц и базовой группой с нулём.

LaTeX

$$OrderIso.withZeroUnits$$

Lean4

/-- Given any linearly ordered commutative group with zero `α`, this is the order isomorphism
between `WithZero αˣ` with `α`. -/
@[simps!]
def withZeroUnits : WithZero αˣ ≃o α where
  __ := withZeroUnitsEquiv
  map_rel_iff' := WithZero.withZeroUnitsEquiv_strictMono.le_iff_le

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