Bundled ordered monoid structures on Multiplicative α and Additive α.

instance Multiplicative.isOrderedMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] : IsOrderedMonoid (Multiplicative α)

instance Additive.isOrderedAddMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] : IsOrderedAddMonoid (Additive α)

instance Multiplicative.isOrderedCancelMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] : IsOrderedCancelMonoid (Multiplicative α)

instance Additive.isOrderedCancelAddMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] : IsOrderedCancelAddMonoid (Additive α)

instance Multiplicative.canonicallyOrderedMul {α : Type u_1} [AddMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] : CanonicallyOrderedMul (Multiplicative α)

instance Additive.canonicallyOrderedAdd {α : Type u_1} [Monoid α] [PartialOrder α] [CanonicallyOrderedMul α] : CanonicallyOrderedAdd (Additive α)