The units of an ordered commutative monoid form an ordered commutative group #
The units of an ordered commutative monoid form an ordered commutative group.
instance
AddUnits.isOrderedAddMonoid
{α : Type u_1}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
:
The units of an ordered commutative additive monoid form an ordered commutative additive group.