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

instance Units.orderedCommGroup {α : Type u_1} [OrderedCommMonoid α] : OrderedCommGroup αˣ

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

Equations

• Units.orderedCommGroup = { toCommGroup := Units.instCommGroupUnits, toPartialOrder := Units.instPartialOrderUnits, mul_le_mul_left := ⋯ }

instance AddUnits.orderedAddCommGroup {α : Type u_1} [OrderedAddCommMonoid α] : OrderedAddCommGroup (AddUnits α)

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

Equations

• AddUnits.orderedAddCommGroup = { toAddCommGroup := AddUnits.instAddCommGroupAddUnits, toPartialOrder := AddUnits.instPartialOrderAddUnits, add_le_add_left := ⋯ }

instance Units.instLinearOrderedCommGroup {α : Type u_1} [LinearOrderedCommMonoid α] : LinearOrderedCommGroup αˣ

The units of a linearly ordered commutative monoid form a linearly ordered commutative group.

Equations

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

instance AddUnits.instLinearOrderedAddCommGroup {α : Type u_1} [LinearOrderedAddCommMonoid α] : LinearOrderedAddCommGroup (AddUnits α)

The units of a linearly ordered commutative additive monoid form a linearly ordered commutative additive group.

Equations

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