# Documentation

Mathlib.Algebra.Order.Monoid.Prod

# Products of ordered monoids #

theorem Prod.instOrderedAddCommMonoidSum.proof_1 {α : Type u_1} {β : Type u_2} :
∀ (x x_1 : α × β), x x_1∀ (x_2 : α × β), (x_2 + x).1 (x_2 + x_1).1 (x_2 + x).2 (x_2 + x_1).2
instance Prod.instOrderedAddCommMonoidSum {α : Type u_1} {β : Type u_2} :
Equations
instance Prod.instOrderedCommMonoidProd {α : Type u_1} {β : Type u_2} :
Equations
theorem Prod.instOrderedAddCancelCommMonoid.proof_2 {α : Type u_1} {β : Type u_2} :
∀ (x x_1 x_2 : α × β), x + x_1 x + x_2x_1.1 x_2.1 x_1.2 x_2.2
theorem Prod.instOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} (a : α × β) (b : α × β) :
a b∀ (c : α × β), c + a c + b
instance Prod.instOrderedAddCancelCommMonoid {α : Type u_1} {β : Type u_2} :
Equations
instance Prod.instOrderedCancelCommMonoid {α : Type u_1} {β : Type u_2} :
Equations
∀ {a b : α × β} (motive : (∃ (c : β), b.2 = a.2 + c)Prop) (x : ∃ (c : β), b.2 = a.2 + c), (∀ (d : β) (hd : b.2 = a.2 + d), motive (_ : ∃ (c : β), b.2 = a.2 + c))motive x
Equations
• (_ : motive x) = (_ : motive x)
Instances For
∀ {a b : α × β} (motive : (∃ (c : α), b.1 = a.1 + c)Prop) (x : ∃ (c : α), b.1 = a.1 + c), (∀ (c : α) (hc : b.1 = a.1 + c), motive (_ : ∃ (c : α), b.1 = a.1 + c))motive x
Equations
• (_ : motive x) = (_ : motive x)
Instances For
Equations
instance Prod.instExistsMulOfLEProdInstMulInstLEProd {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Mul α] [Mul β] [] [] :
Equations
theorem Prod.instCanonicallyOrderedAddCommMonoidSum.proof_5 {α : Type u_1} {β : Type u_2} :
∀ (x x_1 : α × β), x.1 (x + x_1).1 x.2 (x + x_1).2
instance Prod.instCanonicallyOrderedAddCommMonoidSum {α : Type u_1} {β : Type u_2} :
Equations
• One or more equations did not get rendered due to their size.
theorem Prod.instCanonicallyOrderedAddCommMonoidSum.proof_1 {α : Type u_1} {β : Type u_2} (a : α × β) (b : α × β) :
a b∀ (c : α × β), c + a c + b
theorem Prod.instCanonicallyOrderedAddCommMonoidSum.proof_4 {α : Type u_1} {β : Type u_2} :
∀ {a b : α × β}, a b∃ (c : α × β), b = a + c
theorem Prod.instCanonicallyOrderedAddCommMonoidSum.proof_3 {α : Type u_1} {β : Type u_2} (a : α × β) :
instance Prod.instCanonicallyOrderedCommMonoidProd {α : Type u_1} {β : Type u_2} :
Equations
• One or more equations did not get rendered due to their size.
instance Prod.Lex.orderedAddCommMonoid {α : Type u_1} {β : Type u_2} [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] :
Equations
theorem Prod.Lex.orderedAddCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (x : Lex (α × β)) (y : Lex (α × β)) (hxy : x y) (z : Lex (α × β)) :
z + x z + y
instance Prod.Lex.orderedCommMonoid {α : Type u_1} {β : Type u_2} [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] :
Equations
theorem Prod.Lex.orderedAddCancelCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} :
∀ (x x_1 : Lex (α × β)), x x_1∀ (a : Lex (α × β)), a + x a + x_1
theorem Prod.Lex.orderedAddCancelCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} :
∀ (x x_1 x_2 : Lex (α × β)), x + x_1 x + x_2x_1 x_2
Equations
instance Prod.Lex.orderedCancelCommMonoid {α : Type u_1} {β : Type u_2} :
Equations
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} (a : Lex (α × β)) (b : Lex (α × β)) (c : Lex (α × β)) :
a + b a + cb c
Equations
• One or more equations did not get rendered due to their size.
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} (a : Lex (α × β)) (b : Lex (α × β)) :
a b b a
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_4 {α : Type u_2} {β : Type u_1} (a : Lex (α × β)) (b : Lex (α × β)) :
max a b = if a b then b else a
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_5 {α : Type u_2} {β : Type u_1} (a : Lex (α × β)) (b : Lex (α × β)) :
compare a b =
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_3 {α : Type u_2} {β : Type u_1} (a : Lex (α × β)) (b : Lex (α × β)) :
min a b = if a b then a else b
Equations
• One or more equations did not get rendered due to their size.