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.
def AddUnits.orderedAddCommGroup.proof_3 {α : Type u_1} [inst : OrderedAddCommMonoid α] :
∀ (x x_1 : AddUnits α), x x_1∀ (x_2 : AddUnits α), 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 : OrderedAddCommMonoid α] (a : AddUnits α) (b : AddUnits α) :
a + b = b + a
Equations
def AddUnits.orderedAddCommGroup.proof_2 {α : Type u_1} [inst : OrderedAddCommMonoid α] (a : AddUnits α) (b : AddUnits α) :
a bb aa = b
Equations

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.