Documentation

Mathlib.Algebra.Order.Group.Units

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

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.