Ordered monoid structures on the order dual. #
instance
OrderDual.isOrderedMonoid
{α : Type u}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
:
instance
OrderDual.isOrderedAddMonoid
{α : Type u}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
:
instance
OrderDual.isOrderedCancelMonoid
{α : Type u}
[CommMonoid α]
[PartialOrder α]
[IsOrderedCancelMonoid α]
:
instance
OrderDual.isOrderedAddCancelMonoid
{α : Type u}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedCancelAddMonoid α]
: