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

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

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

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

Equations

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

instance Prod.Lex.orderedAddCommGroup {G : Type u_2} {H : Type u_3} [OrderedAddCommGroup G] [OrderedAddCommGroup H] : OrderedAddCommGroup (Lex (G × H))

Equations

• Prod.Lex.orderedAddCommGroup = OrderedAddCommGroup.mk (_ : ∀ (x x_1 : Lex (G × H)), x ≤ x_1 → ∀ (a : Lex (G × H)), a + x ≤ a + x_1)

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

instance Prod.Lex.orderedCommGroup {G : Type u_2} {H : Type u_3} [OrderedCommGroup G] [OrderedCommGroup H] : OrderedCommGroup (Lex (G × H))

Equations

• Prod.Lex.orderedCommGroup = OrderedCommGroup.mk (_ : ∀ (x x_1 : Lex (G × H)), x ≤ x_1 → ∀ (a : Lex (G × H)), a * x ≤ a * x_1)

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_2 {G : Type u_2} {H : Type u_1} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup H] (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} [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

instance Prod.Lex.linearOrderedAddCommGroup {G : Type u_2} {H : Type u_3} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup H] : LinearOrderedAddCommGroup (Lex (G × H))

Equations

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

theorem Prod.Lex.linearOrderedAddCommGroup.proof_5 {G : Type u_2} {H : Type u_1} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup H] (a : Lex (G × H)) (b : Lex (G × H)) : compare a b = compareOfLessAndEq a b

instance Prod.Lex.linearOrderedCommGroup {G : Type u_2} {H : Type u_3} [LinearOrderedCommGroup G] [LinearOrderedCommGroup H] : LinearOrderedCommGroup (Lex (G × H))

Equations

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