← Mathematical handbook

Multisets as ordered monoids

The IsOrderedCancelAddMonoid and CanonicallyOrderedAdd instances on Multiset α

instance Multiset.instIsOrderedCancelAddMonoid {α : Type u_1} : IsOrderedCancelAddMonoid (Multiset α)

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