Products of ordered commutative groups.

ink

def Prod.instOrderedAddCommGroupSum.proof_1 {G : Type u_1} {H : Type u_2} [inst : OrderedAddCommGroup G] [inst : OrderedAddCommGroup H] (a : G × H) (b : G × H) : a + b = b + a

Equations

• (_ : ∀ (a b : G × H), a + b = b + a) = (_ : ∀ (a b : G × H), a + b = b + a)

ink

instance Prod.instOrderedAddCommGroupSum {G : Type u_1} {H : Type u_2} [inst : OrderedAddCommGroup G] [inst : OrderedAddCommGroup H] : OrderedAddCommGroup (G × H)

Equations

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

ink

def Prod.instOrderedAddCommGroupSum.proof_2 {G : Type u_1} {H : Type u_2} [inst : OrderedAddCommGroup G] [inst : OrderedAddCommGroup H] (a : G × H) (b : G × H) : a ≤ b → ∀ (c : G × H), c + a ≤ c + b

Equations

• (_ : ∀ (a b : G × H), a ≤ b → ∀ (c : G × H), c + a ≤ c + b) = (_ : ∀ (a b : G × H), a ≤ b → ∀ (c : G × H), c + a ≤ c + b)

ink

instance Prod.instOrderedCommGroupProd {G : Type u_1} {H : Type u_2} [inst : OrderedCommGroup G] [inst : OrderedCommGroup H] : OrderedCommGroup (G × H)

Equations

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