Bundled ordered monoid structures on Multiplicative α
and Additive α
. #
instance
Multiplicative.canonicallyOrderedMul
{α : Type u_1}
[AddMonoid α]
[PartialOrder α]
[CanonicallyOrderedAdd α]
:
instance
Additive.canonicallyOrderedAdd
{α : Type u_1}
[Monoid α]
[PartialOrder α]
[CanonicallyOrderedMul α]
: