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

ink

instance AddUnits.orderedAddCommGroup {α : Type u_1} [inst : 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.

ink

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)

ink

def AddUnits.orderedAddCommGroup.proof_1 {α : Type u_1} [inst : OrderedAddCommMonoid α] (a : AddUnits α) (b : AddUnits α) : a + b = b + a

Equations

• (_ : ∀ (a b : AddUnits α), a + b = b + a) = (_ : ∀ (a b : AddUnits α), a + b = b + a)

ink

def AddUnits.orderedAddCommGroup.proof_2 {α : Type u_1} [inst : OrderedAddCommMonoid α] (a : AddUnits α) (b : AddUnits α) : a ≤ b → b ≤ a → a = b

Equations

• (_ : ∀ (a b : AddUnits α), a ≤ b → b ≤ a → a = b) = (_ : ∀ (a b : AddUnits α), a ≤ b → b ≤ a → a = b)

ink

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

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.