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.

theorem AddUnits.orderedAddCommGroup.proof_3 {α : Type u_1} [OrderedAddCommMonoid α] :
∀ (x x_1 : AddUnits α), x x_1∀ (x_2 : AddUnits α), x_2 + x x_2 + x_1
theorem AddUnits.orderedAddCommGroup.proof_1 {α : Type u_1} [OrderedAddCommMonoid α] (a : AddUnits α) (b : AddUnits α) :
a + b = b + a
theorem AddUnits.orderedAddCommGroup.proof_2 {α : Type u_1} [OrderedAddCommMonoid α] (a : AddUnits α) (b : AddUnits α) :
a bb aa = b

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