Documentation

Mathlib.Algebra.Order.Monoid.Prod

Products of ordered monoids #

def Prod.instOrderedAddCommMonoidSum.proof_1 {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] :
∀ (x x_1 : α × β), x x_1∀ (x_2 : α × β), (x_2 + x).fst (x_2 + x_1).fst (x_2 + x).snd (x_2 + x_1).snd
Equations
instance Prod.instOrderedAddCommMonoidSum {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] :
Equations
instance Prod.instOrderedCommMonoidProd {α : Type u_1} {β : Type u_2} [inst : OrderedCommMonoid α] [inst : OrderedCommMonoid β] :
Equations
def Prod.instOrderedAddCancelCommMonoidSum.proof_1 {M : Type u_1} {N : Type u_2} [inst : OrderedCancelAddCommMonoid M] [inst : OrderedCancelAddCommMonoid N] (a : M × N) (b : M × N) :
a b∀ (c : M × N), c + a c + b
Equations
  • (_ : ∀ (a b : M × N), a b∀ (c : M × N), c + a c + b) = (_ : ∀ (a b : M × N), a b∀ (c : M × N), c + a c + b)
Equations
  • One or more equations did not get rendered due to their size.
def Prod.instOrderedAddCancelCommMonoidSum.proof_2 {M : Type u_1} {N : Type u_2} [inst : OrderedCancelAddCommMonoid M] [inst : OrderedCancelAddCommMonoid N] :
∀ (x x_1 x_2 : M × N), x + x_1 x + x_2x_1.fst x_2.fst x_1.snd x_2.snd
Equations
Equations
  • One or more equations did not get rendered due to their size.
def Prod.instExistsAddOfLESumInstAddSumInstLESum.proof_1 {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] [inst : Add α] [inst : Add β] [inst : ExistsAddOfLE α] [inst : ExistsAddOfLE β] :
Equations
abbrev Prod.instExistsAddOfLESumInstAddSumInstLESum.match_2 {α : Type u_1} {β : Type u_2} [inst : Add α] :
{a b : α × β} → (motive : (c, b.fst = a.fst + c) → Prop) → ∀ (x : c, b.fst = a.fst + c), (∀ (c : α) (hc : b.fst = a.fst + c), motive (_ : c, b.fst = a.fst + c)) → motive x
Equations
abbrev Prod.instExistsAddOfLESumInstAddSumInstLESum.match_1 {α : Type u_2} {β : Type u_1} [inst : Add β] :
{a b : α × β} → (motive : (c, b.snd = a.snd + c) → Prop) → ∀ (x : c, b.snd = a.snd + c), (∀ (d : β) (hd : b.snd = a.snd + d), motive (_ : c, b.snd = a.snd + c)) → motive x
Equations
def Prod.instCanonicallyOrderedAddMonoidSum.proof_4 {α : Type u_1} {β : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : CanonicallyOrderedAddMonoid β] :
∀ {a b : α × β}, a bc, b = a + c
Equations
  • (_ : a bc, b = a + c) = (_ : a bc, b = a + c)
Equations
def Prod.instCanonicallyOrderedAddMonoidSum.proof_1 {α : Type u_1} {β : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : CanonicallyOrderedAddMonoid β] (a : α × β) (b : α × β) :
a b∀ (c : α × β), c + a c + b
Equations
  • (_ : ∀ (a b : α × β), a b∀ (c : α × β), c + a c + b) = (_ : ∀ (a b : α × β), a b∀ (c : α × β), c + a c + b)
Equations
  • One or more equations did not get rendered due to their size.
def Prod.instCanonicallyOrderedAddMonoidSum.proof_5 {α : Type u_1} {β : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : CanonicallyOrderedAddMonoid β] :
∀ (x x_1 : α × β), x.fst (x + x_1).fst x.snd (x + x_1).snd
Equations
Equations
  • One or more equations did not get rendered due to their size.