Products of ordered monoids

instance Prod.instOrderedCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCommMonoid α] [OrderedCommMonoid β] : OrderedCommMonoid (α × β)

Equations

• Prod.instOrderedCommMonoid = OrderedCommMonoid.mk ⋯

instance Prod.instOrderedAddCommMonoid {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] : OrderedAddCommMonoid (α × β)

Equations

• Prod.instOrderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

instance Prod.instOrderedCancelCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCancelCommMonoid α] [OrderedCancelCommMonoid β] : OrderedCancelCommMonoid (α × β)

Equations

• Prod.instOrderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

instance Prod.instOrderedAddCancelCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] : OrderedCancelAddCommMonoid (α × β)

Equations

• Prod.instOrderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

instance Prod.instExistsMulOfLE {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Mul α] [Mul β] [ExistsMulOfLE α] [ExistsMulOfLE β] : ExistsMulOfLE (α × β)

instance Prod.instExistsAddOfLE {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Add α] [Add β] [ExistsAddOfLE α] [ExistsAddOfLE β] : ExistsAddOfLE (α × β)

instance Prod.instCanonicallyOrderedMul {α : Type u_1} {β : Type u_2} [Mul α] [LE α] [CanonicallyOrderedMul α] [Mul β] [LE β] [CanonicallyOrderedMul β] : CanonicallyOrderedMul (α × β)

instance Prod.instCanonicallyOrderedAdd {α : Type u_1} {β : Type u_2} [Add α] [LE α] [CanonicallyOrderedAdd α] [Add β] [LE β] [CanonicallyOrderedAdd β] : CanonicallyOrderedAdd (α × β)

instance Prod.Lex.orderedCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCommMonoid α] [MulLeftStrictMono α] [OrderedCommMonoid β] : OrderedCommMonoid (Lex (α × β))

Equations

• Prod.Lex.orderedCommMonoid = OrderedCommMonoid.mk ⋯

instance Prod.Lex.orderedAddCommMonoid {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid α] [AddLeftStrictMono α] [OrderedAddCommMonoid β] : OrderedAddCommMonoid (Lex (α × β))

Equations

• Prod.Lex.orderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

instance Prod.Lex.orderedCancelCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCancelCommMonoid α] [OrderedCancelCommMonoid β] : OrderedCancelCommMonoid (Lex (α × β))

Equations

• Prod.Lex.orderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

instance Prod.Lex.orderedAddCancelCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] : OrderedCancelAddCommMonoid (Lex (α × β))

Equations

• Prod.Lex.orderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

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 ⋯ ⋯ ⋯

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 ⋯ ⋯ ⋯