Finsupp.toMultiset the equivalence between
α →₀ ℕ and
Multiset α, along
Multiset.toFinsupp the reverse equivalence and
Finsupp.orderIsoMultiset the equivalence
promoted to an order isomorphism.
Under the additional assumption of
[DecidableEq α], this is available as
Multiset.toFinsupp : Multiset α ≃+ (α →₀ ℕ); the two declarations are separate as this assumption
is only needed for one direction.