Products of ordered monoids #
instance
Prod.instOrderedAddCommMonoid
{α : Type u_1}
{β : Type u_2}
[OrderedAddCommMonoid α]
[OrderedAddCommMonoid β]
:
OrderedAddCommMonoid (α × β)
Equations
- Prod.instOrderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯
instance
Prod.instOrderedCommMonoid
{α : Type u_1}
{β : Type u_2}
[OrderedCommMonoid α]
[OrderedCommMonoid β]
:
OrderedCommMonoid (α × β)
Equations
- Prod.instOrderedCommMonoid = OrderedCommMonoid.mk ⋯
instance
Prod.instOrderedAddCancelCommMonoid
{α : Type u_1}
{β : Type u_2}
[OrderedCancelAddCommMonoid α]
[OrderedCancelAddCommMonoid β]
:
OrderedCancelAddCommMonoid (α × β)
Equations
- Prod.instOrderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯
theorem
Prod.instOrderedAddCancelCommMonoid.proof_1
{α : Type u_1}
{β : Type u_2}
[OrderedCancelAddCommMonoid α]
[OrderedCancelAddCommMonoid β]
:
instance
Prod.instOrderedCancelCommMonoid
{α : Type u_1}
{β : Type u_2}
[OrderedCancelCommMonoid α]
[OrderedCancelCommMonoid β]
:
OrderedCancelCommMonoid (α × β)
Equations
- Prod.instOrderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯
instance
Prod.instExistsAddOfLE
{α : Type u_1}
{β : Type u_2}
[LE α]
[LE β]
[Add α]
[Add β]
[ExistsAddOfLE α]
[ExistsAddOfLE β]
:
ExistsAddOfLE (α × β)
Equations
- ⋯ = ⋯
instance
Prod.instExistsMulOfLE
{α : Type u_1}
{β : Type u_2}
[LE α]
[LE β]
[Mul α]
[Mul β]
[ExistsMulOfLE α]
[ExistsMulOfLE β]
:
ExistsMulOfLE (α × β)
Equations
- ⋯ = ⋯
instance
Prod.instCanonicallyOrderedAddCommMonoid
{α : Type u_1}
{β : Type u_2}
[CanonicallyOrderedAddCommMonoid α]
[CanonicallyOrderedAddCommMonoid β]
:
Equations
- Prod.instCanonicallyOrderedAddCommMonoid = CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯
theorem
Prod.instCanonicallyOrderedAddCommMonoid.proof_2
{α : Type u_1}
{β : Type u_2}
[CanonicallyOrderedAddCommMonoid α]
[CanonicallyOrderedAddCommMonoid β]
:
theorem
Prod.instCanonicallyOrderedAddCommMonoid.proof_1
{α : Type u_1}
{β : Type u_2}
[CanonicallyOrderedAddCommMonoid α]
[CanonicallyOrderedAddCommMonoid β]
:
ExistsAddOfLE (α × β)
theorem
Prod.instCanonicallyOrderedAddCommMonoid.proof_3
{α : Type u_1}
{β : Type u_2}
[CanonicallyOrderedAddCommMonoid α]
[CanonicallyOrderedAddCommMonoid β]
:
instance
Prod.instCanonicallyOrderedCommMonoid
{α : Type u_1}
{β : Type u_2}
[CanonicallyOrderedCommMonoid α]
[CanonicallyOrderedCommMonoid β]
:
Equations
- Prod.instCanonicallyOrderedCommMonoid = CanonicallyOrderedCommMonoid.mk ⋯ ⋯
instance
Prod.Lex.orderedAddCommMonoid
{α : Type u_1}
{β : Type u_2}
[OrderedAddCommMonoid α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2]
[OrderedAddCommMonoid β]
:
OrderedAddCommMonoid (Lex (α × β))
Equations
- Prod.Lex.orderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯
theorem
Prod.Lex.orderedAddCommMonoid.proof_1
{α : Type u_2}
{β : Type u_1}
[OrderedAddCommMonoid α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2]
[OrderedAddCommMonoid β]
:
instance
Prod.Lex.orderedCommMonoid
{α : Type u_1}
{β : Type u_2}
[OrderedCommMonoid α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2]
[OrderedCommMonoid β]
:
OrderedCommMonoid (Lex (α × β))
Equations
- Prod.Lex.orderedCommMonoid = OrderedCommMonoid.mk ⋯
theorem
Prod.Lex.orderedAddCancelCommMonoid.proof_1
{α : Type u_2}
{β : Type u_1}
[OrderedCancelAddCommMonoid α]
[OrderedCancelAddCommMonoid β]
:
instance
Prod.Lex.orderedAddCancelCommMonoid
{α : Type u_1}
{β : Type u_2}
[OrderedCancelAddCommMonoid α]
[OrderedCancelAddCommMonoid β]
:
OrderedCancelAddCommMonoid (Lex (α × β))
Equations
- Prod.Lex.orderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯
theorem
Prod.Lex.orderedAddCancelCommMonoid.proof_2
{α : Type u_2}
{β : Type u_1}
[OrderedCancelAddCommMonoid α]
[OrderedCancelAddCommMonoid β]
:
instance
Prod.Lex.orderedCancelCommMonoid
{α : Type u_1}
{β : Type u_2}
[OrderedCancelCommMonoid α]
[OrderedCancelCommMonoid β]
:
OrderedCancelCommMonoid (Lex (α × β))
Equations
- Prod.Lex.orderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯
theorem
Prod.Lex.linearOrderedAddCancelCommMonoid.proof_4
{α : Type u_2}
{β : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
[LinearOrderedCancelAddCommMonoid β]
(a : Lex (α × β))
(b : Lex (α × β))
:
instance
Prod.Lex.linearOrderedAddCancelCommMonoid
{α : Type u_1}
{β : Type u_2}
[LinearOrderedCancelAddCommMonoid α]
[LinearOrderedCancelAddCommMonoid β]
:
LinearOrderedCancelAddCommMonoid (Lex (α × β))
Equations
- Prod.Lex.linearOrderedAddCancelCommMonoid = LinearOrderedCancelAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯
theorem
Prod.Lex.linearOrderedAddCancelCommMonoid.proof_6
{α : Type u_2}
{β : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
[LinearOrderedCancelAddCommMonoid β]
(a : Lex (α × β))
(b : Lex (α × β))
:
compare a b = compareOfLessAndEq a b
theorem
Prod.Lex.linearOrderedAddCancelCommMonoid.proof_3
{α : Type u_2}
{β : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
[LinearOrderedCancelAddCommMonoid β]
(a : Lex (α × β))
(b : Lex (α × β))
:
theorem
Prod.Lex.linearOrderedAddCancelCommMonoid.proof_5
{α : Type u_2}
{β : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
[LinearOrderedCancelAddCommMonoid β]
(a : Lex (α × β))
(b : Lex (α × β))
:
instance
Prod.Lex.linearOrderedCancelCommMonoid
{α : Type u_1}
{β : Type u_2}
[LinearOrderedCancelCommMonoid α]
[LinearOrderedCancelCommMonoid β]
:
LinearOrderedCancelCommMonoid (Lex (α × β))
Equations
- Prod.Lex.linearOrderedCancelCommMonoid = LinearOrderedCancelCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯