English
A linearly ordered group with zero has an isomorphism between its unit group of WithZero and the group itself; i.e., WithZeroUnitsEquiv provides an order-monoid isomorphism between WithZero αˣ and α.
Русский
Линейно упорядоченная группа с нулём эквивариантна между единицами WithZero αˣ и самой α; существует упорядоченный моноидовый изоморфизм WithZeroUnitsEquiv.
LaTeX
$$$(WithZero\\,\\alpha)^{\\times} \\cong_o \\alpha$$$
Lean4
/-- Any linearly ordered group with zero is isomorphic to adjoining `0` to the units of itself. -/
@[simps!]
def withZeroUnits {α : Type*} [LinearOrderedCommGroupWithZero α] [DecidablePred (fun a : α ↦ a = 0)] : WithZero αˣ ≃*o α
where
toMulEquiv := WithZero.withZeroUnitsEquiv
map_le_map_iff' {a b} := by cases a <;> cases b <;> simp
