# Documentation

Mathlib.Algebra.Order.Group.Units

# 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
• One or more equations did not get rendered due to their size.
∀ (x x_1 : ), x x_1∀ (x_2 : ), x_2 + x x_2 + x_1
Equations
• (_ : x + x x + x) = (_ : x + x x + x)
def AddUnits.orderedAddCommGroup.proof_1 {α : Type u_1} [inst : ] (a : ) (b : ) :
a + b = b + a
Equations
• (_ : ∀ (a b : ), a + b = b + a) = (_ : ∀ (a b : ), a + b = b + a)
def AddUnits.orderedAddCommGroup.proof_2 {α : Type u_1} [inst : ] (a : ) (b : ) :
a bb aa = b
Equations
• (_ : ∀ (a b : ), a bb aa = b) = (_ : ∀ (a b : ), a bb aa = b)
instance Units.orderedCommGroup {α : Type u_1} [inst : ] :

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

Equations
• One or more equations did not get rendered due to their size.