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 → ∀ (c : G × H), c + a ≤ c + b

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

Equations

• Prod.instOrderedAddCommGroupSum = let __src := Prod.instAddCommGroup; let __src_1 := Prod.instPartialOrder G H; let __src_2 := Prod.instOrderedAddCancelCommMonoid; OrderedAddCommGroup.mk ⋯

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

Equations

• Prod.instOrderedCommGroupProd = let __src := Prod.instCommGroup; let __src_1 := Prod.instPartialOrder G H; let __src_2 := Prod.instOrderedCancelCommMonoid; OrderedCommGroup.mk ⋯

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.orderedAddCommGroup {G : Type u_2} {H : Type u_3} [OrderedAddCommGroup G] [OrderedAddCommGroup H] : OrderedAddCommGroup (Lex (G × H))

Equations

• Prod.Lex.orderedAddCommGroup = OrderedAddCommGroup.mk ⋯

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 ⋯

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

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

• Prod.Lex.linearOrderedAddCommGroup = let __spread.0 := inferInstance; LinearOrderedAddCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

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

Equations

• Prod.Lex.linearOrderedCommGroup = let __spread.0 := inferInstance; LinearOrderedCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯