Equivalence between Multiset
and ℕ
-valued finitely supported functions #
This defines Finsupp.toMultiset
the equivalence between α →₀ ℕ
and Multiset α
, along
with Multiset.toFinsupp
the reverse equivalence and Finsupp.orderIsoMultiset
the equivalence
promoted to an order isomorphism.
Given f : α →₀ ℕ
, f.toMultiset
is the multiset with multiplicities given by the values of
f
on the elements of α
. We define this function as an AddMonoidHom
.
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.
Instances For
Given a multiset s
, s.toFinsupp
returns the finitely supported function on ℕ
given by
the multiplicities of the elements of s
.
Instances For
As an order isomorphism #
Finsupp.toMultiset
as an order isomorphism.