Products of ordered monoids #
def
Prod.instOrderedAddCommMonoidSum.proof_1
{α : Type u_1}
{β : Type u_2}
[inst : OrderedAddCommMonoid α]
[inst : OrderedAddCommMonoid β]
:
instance
Prod.instOrderedAddCommMonoidSum
{α : Type u_1}
{β : Type u_2}
[inst : OrderedAddCommMonoid α]
[inst : OrderedAddCommMonoid β]
:
OrderedAddCommMonoid (α × β)
instance
Prod.instOrderedCommMonoidProd
{α : Type u_1}
{β : Type u_2}
[inst : OrderedCommMonoid α]
[inst : OrderedCommMonoid β]
:
OrderedCommMonoid (α × β)
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)
:
instance
Prod.instOrderedAddCancelCommMonoidSum
{M : Type u_1}
{N : Type u_2}
[inst : OrderedCancelAddCommMonoid M]
[inst : OrderedCancelAddCommMonoid N]
:
OrderedCancelAddCommMonoid (M × N)
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]
:
instance
Prod.instOrderedCancelCommMonoidProd
{M : Type u_1}
{N : Type u_2}
[inst : OrderedCancelCommMonoid M]
[inst : OrderedCancelCommMonoid N]
:
OrderedCancelCommMonoid (M × N)
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 β]
:
ExistsAddOfLE (α × β)
Equations
- (_ : ExistsAddOfLE (α × β)) = (_ : ExistsAddOfLE (α × β))
abbrev
Prod.instExistsAddOfLESumInstAddSumInstLESum.match_2
{α : Type u_1}
{β : Type u_2}
[inst : Add α]
:
Equations
- Prod.instExistsAddOfLESumInstAddSumInstLESum.match_2 motive x h_1 = Exists.casesOn x fun w h => h_1 w h
abbrev
Prod.instExistsAddOfLESumInstAddSumInstLESum.match_1
{α : Type u_2}
{β : Type u_1}
[inst : Add β]
:
Equations
- Prod.instExistsAddOfLESumInstAddSumInstLESum.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h
instance
Prod.instExistsAddOfLESumInstAddSumInstLESum
{α : Type u_1}
{β : Type u_2}
[inst : LE α]
[inst : LE β]
[inst : Add α]
[inst : Add β]
[inst : ExistsAddOfLE α]
[inst : ExistsAddOfLE β]
:
ExistsAddOfLE (α × β)
instance
Prod.instExistsMulOfLEProdInstMulProdInstLEProd
{α : Type u_1}
{β : Type u_2}
[inst : LE α]
[inst : LE β]
[inst : Mul α]
[inst : Mul β]
[inst : ExistsMulOfLE α]
[inst : ExistsMulOfLE β]
:
ExistsMulOfLE (α × β)
def
Prod.instCanonicallyOrderedAddMonoidSum.proof_2
{α : Type u_1}
{β : Type u_2}
[inst : CanonicallyOrderedAddMonoid α]
[inst : CanonicallyOrderedAddMonoid β]
:
ExistsAddOfLE (α × β)
Equations
- (_ : ExistsAddOfLE (α × β)) = (_ : ExistsAddOfLE (α × β))
def
Prod.instCanonicallyOrderedAddMonoidSum.proof_1
{α : Type u_1}
{β : Type u_2}
[inst : CanonicallyOrderedAddMonoid α]
[inst : CanonicallyOrderedAddMonoid β]
(a : α × β)
(b : α × β)
:
instance
Prod.instCanonicallyOrderedAddMonoidSum
{α : Type u_1}
{β : Type u_2}
[inst : CanonicallyOrderedAddMonoid α]
[inst : CanonicallyOrderedAddMonoid β]
:
CanonicallyOrderedAddMonoid (α × β)
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 β]
:
instance
Prod.instCanonicallyOrderedMonoidProd
{α : Type u_1}
{β : Type u_2}
[inst : CanonicallyOrderedMonoid α]
[inst : CanonicallyOrderedMonoid β]
:
CanonicallyOrderedMonoid (α × β)
Equations
- One or more equations did not get rendered due to their size.