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

theorem AddUnits.orderedAddCommGroup.proof_1 {α : Type u_1} [OrderedAddCommMonoid α] : ∀ (x x_1 : AddUnits α), x ≤ x_1 → ∀ (x_2 : AddUnits α), ↑x_2 + ↑x ≤ ↑x_2 + ↑x_1

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 = let __src := AddUnits.instPartialOrderAddUnits; let __src_1 := AddUnits.instAddCommGroupAddUnits; OrderedAddCommGroup.mk ⋯

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

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

Equations

• Units.orderedCommGroup = let __src := Units.instPartialOrderUnits; let __src_1 := Units.instCommGroupUnits; OrderedCommGroup.mk ⋯