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

instance Units.isOrderedMonoid {α : Type u_1} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] : IsOrderedMonoid αˣ

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

instance AddUnits.isOrderedAddMonoid {α : Type u_1} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid (AddUnits α)

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