# Bundled ordered monoid structures on `Multiplicative α` and `Additive α`. #

source
instance Multiplicative.isOrderedMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] :
IsOrderedMonoid (Multiplicative α)
source
instance Additive.isOrderedAddMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] :
IsOrderedAddMonoid (Additive α)
source
instance Multiplicative.isOrderedCancelMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] :
IsOrderedCancelMonoid (Multiplicative α)
source
instance Additive.isOrderedCancelAddMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] :
IsOrderedCancelAddMonoid (Additive α)
source
instance Multiplicative.canonicallyOrderedMul {α : Type u_1} [AddMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] :
CanonicallyOrderedMul (Multiplicative α)
source
instance Additive.canonicallyOrderedAdd {α : Type u_1} [Monoid α] [PartialOrder α] [CanonicallyOrderedMul α] :
CanonicallyOrderedAdd (Additive α)