Documentation

Mathlib.Algebra.Order.Group.Prod

Products of ordered commutative groups. #

theorem Prod.instOrderedAddCommGroupSum.proof_1 {G : Type u_1} {H : Type u_2} [OrderedAddCommGroup G] [OrderedAddCommGroup H] (a : G × H) (b : G × H) :
a + b = b + a
Equations
  • One or more equations did not get rendered due to their size.
theorem Prod.instOrderedAddCommGroupSum.proof_2 {G : Type u_1} {H : Type u_2} [OrderedAddCommGroup G] [OrderedAddCommGroup H] (a : G × H) (b : G × H) :
a b∀ (c : G × H), c + a c + b
Equations
  • One or more equations did not get rendered due to their size.
Equations
theorem Prod.Lex.orderedAddCommGroup.proof_1 {G : Type u_2} {H : Type u_1} [OrderedAddCommGroup G] [OrderedAddCommGroup H] :
∀ (x x_1 : Lex (G × H)), x x_1∀ (a : Lex (G × H)), a + x a + x_1
Equations
theorem Prod.Lex.linearOrderedAddCommGroup.proof_4 {G : Type u_2} {H : Type u_1} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup H] (a : Lex (G × H)) (b : Lex (G × H)) :
max a b = if a b then b else a
theorem Prod.Lex.linearOrderedAddCommGroup.proof_3 {G : Type u_2} {H : Type u_1} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup H] (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} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup H] :
∀ (x x_1 : Lex (G × H)), x x_1∀ (a : Lex (G × H)), a + x a + x_1
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.