Multisets as ordered monoids

The OrderedCancelAddCommMonoid and CanonicallyOrderedAddCommMonoid instances on Multiset α

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

Equations

• Multiset.instOrderedCancelAddCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

instance Multiset.instCanonicallyOrderedAddCommMonoid {α : Type u_1} : CanonicallyOrderedAddCommMonoid (Multiset α)

Equations

• Multiset.instCanonicallyOrderedAddCommMonoid = let __spread.0 := inferInstanceAs (OrderBot (Multiset α)); CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯