Multisets as ordered monoids

The OrderedCancelAddCommMonoid and CanonicallyOrderedAdd instances on Multiset α

instance Multiset.instOrderedCancelAddCommMonoid {α : Type u_1} : OrderedCancelAddCommMonoid (Multiset α)

Equations

• Multiset.instOrderedCancelAddCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

instance Multiset.instCanonicallyOrderedAdd {α : Type u_1} : CanonicallyOrderedAdd (Multiset α)