The units of an ordered commutative monoid form an ordered commutative group #
The units of an ordered commutative additive monoid form an ordered commutative additive group.
Equations
- AddUnits.orderedAddCommGroup = OrderedAddCommGroup.mk ⋯
The units of an ordered commutative monoid form an ordered commutative group.
Equations
- Units.orderedCommGroup = OrderedCommGroup.mk ⋯