Products of ordered monoids #
instance
Prod.instIsOrderedMonoid
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[CommMonoid β]
[PartialOrder β]
[IsOrderedMonoid β]
:
IsOrderedMonoid (α × β)
instance
Prod.instIsOrderedAddMonoid
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[AddCommMonoid β]
[PartialOrder β]
[IsOrderedAddMonoid β]
:
IsOrderedAddMonoid (α × β)
instance
Prod.instIsOrderedCancelMonoid
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[PartialOrder α]
[IsOrderedCancelMonoid α]
[CommMonoid β]
[PartialOrder β]
[IsOrderedCancelMonoid β]
:
IsOrderedCancelMonoid (α × β)
instance
Prod.instIsOrderedAddCancelMonoid
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedCancelAddMonoid α]
[AddCommMonoid β]
[PartialOrder β]
[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 α]
[PartialOrder α]
[MulLeftStrictMono α]
[CommMonoid β]
[PartialOrder β]
[IsOrderedMonoid β]
:
IsOrderedMonoid (Lex (α × β))
instance
Prod.Lex.isOrderedAddMonoid
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[PartialOrder α]
[AddLeftStrictMono α]
[AddCommMonoid β]
[PartialOrder β]
[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 (α × β))