Theorems · Definition · combinatorics
Multiset.toFinsupp
{α : Type u_1} → [DecidableEq α] → Multiset α ≃+ (α →₀ ℕ)Given a multiset s, s.toFinsupp returns the finitely supported function on ℕ given by
the multiplicities of the elements of s.
- Defined in
- Mathlib.Data.Finsupp.Multiset
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Finsuppstatement and proof · cited by 5,255
- Multisetstatement and proof · cited by 2,627
- AddEquivstatement · cited by 1,087
- Multiset.countproof · cited by 302
- Multiset.toFinsetproof · cited by 230
- Finsupp.toMultisetproof · cited by 44
Cited by39
Results whose statement or proof uses this declaration.
- Nat.prod_factorization_pow_eq_selfproof · cited by 22
- factorizationproof · cited by 9
- Multiset.countPermsproof · cited by 8
- Nat.Partition.genFunproof · cited by 5
- Multiset.toFinsupp_toMultisetstatement and proof · cited by 4
- Nat.Partition.hasProd_genFunproof · cited by 4
- Finsupp.orderIsoMultisetproof · cited by 4
- Sym.equivNatSumproof · cited by 3
- Multiset.toFinsupp_applystatement · cited by 2
- Nat.factorization_eq_primeFactorsList_multisetstatement · cited by 2
- Multiset.countPerms_filter_neproof · cited by 2
- Multiset.countPerms_zeroproof · cited by 2