# Documentation

Mathlib.Algebra.Order.Group.Prod

# Products of ordered commutative groups. #

theorem Prod.instOrderedAddCommGroupSum.proof_1 {G : Type u_1} {H : Type u_2} (a : G × H) (b : G × H) :
a + b = b + a
theorem Prod.instOrderedAddCommGroupSum.proof_2 {G : Type u_1} {H : Type u_2} (a : G × H) (b : G × H) :
a b∀ (c : G × H), c + a c + b
instance Prod.instOrderedCommGroupProd {G : Type u_2} {H : Type u_3} [] [] :
theorem Prod.Lex.orderedAddCommGroup.proof_1 {G : Type u_2} {H : Type u_1} :
∀ (x x_1 : Lex (G × H)), x x_1∀ (a : Lex (G × H)), a + x a + x_1
instance Prod.Lex.orderedCommGroup {G : Type u_2} {H : Type u_3} [] [] :
theorem Prod.Lex.linearOrderedAddCommGroup.proof_4 {G : Type u_2} {H : Type u_1} (a : Lex (G × H)) (b : Lex (G × H)) :
max a b = if a b then b else a
theorem Prod.Lex.linearOrderedAddCommGroup.proof_2 {G : Type u_2} {H : Type u_1} (a : Lex (G × H)) (b : Lex (G × H)) :
a b b a
theorem Prod.Lex.linearOrderedAddCommGroup.proof_3 {G : Type u_2} {H : Type u_1} (a : Lex (G × H)) (b : Lex (G × H)) :
min a b = if a b then a else b
theorem Prod.Lex.linearOrderedAddCommGroup.proof_1 {G : Type u_2} {H : Type u_1} :
∀ (x x_1 : Lex (G × H)), x x_1∀ (a : Lex (G × H)), a + x a + x_1
theorem Prod.Lex.linearOrderedAddCommGroup.proof_5 {G : Type u_2} {H : Type u_1} (a : Lex (G × H)) (b : Lex (G × H)) :
compare a b =