unitsWithZero — Mathlib

English

For any ordered group α, there is an order-monoid-isomorphism between the unit group of WithZero α and α itself. Concretely, (Units (WithZero α)) ≃*o α, given by the natural correspondence with WithZero units.

Русский

Для любого упорядоченного группы α существует упорядоченный моноидовый изоморфизм между группой единиц WithZero α и самой α. Формально: (Units (WithZero α)) ≃*o α.

LaTeX

$$$ (Units(\\mathrm{WithZero}\\ \\alpha)) \\cong^o \\alpha $$$

Lean4

/-- Any ordered group is isomorphic to the units of itself adjoined with `0`. -/
@[simps!]
def unitsWithZero {α : Type*} [Group α] [Preorder α] : (WithZero α)ˣ ≃*o α
    where
  toMulEquiv := WithZero.unitsWithZeroEquiv
  map_le_map_iff' {a b} := by simp [WithZero.unitsWithZeroEquiv]

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