Documentation

Mathlib.Algebra.Order.Group.Prod

Products of ordered commutative groups. #

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)
Equations
  • One or more equations did not get rendered due to their size.
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)
instance Prod.instOrderedCommGroupProd {G : Type u_1} {H : Type u_2} [inst : OrderedCommGroup G] [inst : OrderedCommGroup H] :
Equations
  • One or more equations did not get rendered due to their size.