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

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

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.

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 ≤ b → b ≤ a → a = b

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 (_ : ∀ (x x_1 : αˣ), x ≤ x_1 → ∀ (x_2 : αˣ), ↑x_2 * ↑x ≤ ↑x_2 * ↑x_1)