Products of ordered monoids

instance Prod.instIsOrderedMonoid {α : Type u_1} {β : Type u_2} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] [CommMonoid β] [Preorder β] [IsOrderedMonoid β] : IsOrderedMonoid (α × β)

instance Prod.instIsOrderedAddMonoid {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] : IsOrderedAddMonoid (α × β)

instance Prod.instIsOrderedCancelMonoid {α : Type u_1} {β : Type u_2} [CommMonoid α] [Preorder α] [IsOrderedCancelMonoid α] [CommMonoid β] [Preorder β] [IsOrderedCancelMonoid β] : IsOrderedCancelMonoid (α × β)

instance Prod.instIsOrderedAddCancelMonoid {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [Preorder α] [IsOrderedCancelAddMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedCancelAddMonoid β] : IsOrderedCancelAddMonoid (α × β)

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.isOrderedMonoid {α : Type u_1} {β : Type u_2} [CommMonoid α] [Preorder α] [MulLeftStrictMono α] [CommMonoid β] [Preorder β] [IsOrderedMonoid β] : IsOrderedMonoid (Lex (α × β))

instance Prod.Lex.isOrderedAddMonoid {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [Preorder α] [AddLeftStrictMono α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] : IsOrderedAddMonoid (Lex (α × β))

instance Prod.Lex.isOrderedCancelMonoid {α : Type u_1} {β : Type u_2} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [CommMonoid β] [PartialOrder β] [IsOrderedCancelMonoid β] : IsOrderedCancelMonoid (Lex (α × β))

instance Prod.Lex.isOrderedAddCancelMonoid {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] : IsOrderedCancelAddMonoid (Lex (α × β))