isOrderedMonoid — Mathlib

English

The units of an ordered commutative monoid form an ordered commutative group.

Русский

Единицы упорядоченного коммутативного моноида образуют упорядоченную коммутативную группу.

LaTeX

$$$ \alpha^{\times} ext{ is an ordered abelian group} $$$

Lean4

/-- The units of an ordered commutative monoid form an ordered commutative group. -/
@[to_additive /-- The units of an ordered commutative additive monoid form an ordered commutative
          additive group. -/
    ]
instance isOrderedMonoid [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] : IsOrderedMonoid αˣ :=
  { mul_le_mul_left := fun _ _ h _ => (mul_le_mul_left' (α := α) h _) }

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