Multisets as ordered monoids #
The OrderedCancelAddCommMonoid
and CanonicallyOrderedAddCommMonoid
instances on Multiset α
Equations
- Multiset.instOrderedCancelAddCommMonoid = OrderedCancelAddCommMonoid.mk ⋯
Equations
- Multiset.instCanonicallyOrderedAddCommMonoid = let __spread.0 := inferInstanceAs (OrderBot (Multiset α)); CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯