Theorems · Definition · combinatorics

Finsupp.toMultiset

{α : Type u_1} → (α →₀ ℕ) →+ Multiset α

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.

Defined in

Mathlib.Data.Finsupp.Multiset

Cited by

44 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound