Theorems · Theorem · combinatorics
Finsupp.count_toMultiset
∀ {α : Type u_1} [inst : DecidableEq α] (f : α →₀ ℕ) (a : α), Multiset.count a (Finsupp.toMultiset f) = f a- Defined in
- Mathlib.Data.Finsupp.Multiset
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 74 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.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Finsuppstatement and proof · cited by 5,255
- mul_oneproof · cited by 3,885
- AddMonoidHomstatement · cited by 3,230
- Multisetstatement and proof · cited by 2,627
- MulZeroClass.mul_zeroproof · cited by 2,091
- MulZeroClass.zero_mulproof · cited by 1,625
- Finsupp.supportproof · cited by 828
- Finsupp.sumproof · cited by 481
- map_sumproof · cited by 455
- Multiset.countstatement and proof · cited by 302
- Finsupp.toMultisetstatement · cited by 44
Cited by10
Results whose statement or proof uses this declaration.
- MvPolynomial.degreeOf_eq_supproof · cited by 15
- MvPolynomial.degreeOf_monomial_eqproof · cited by 1
- MvPolynomial.mem_restrictDegree_iff_supproof · cited by 1
- ChevalleyThm.chevalley_mvPolynomialCproof · cited by 1
- Finset.count_coe_finsuppAntidiagEquiv_applyproof · cited by 0
- Finsupp.toMultiset_infproof · cited by 0
- Finsupp.toMultiset_supproof · cited by 0
- MvPolynomial.weightedTotalDegree_piSingleproof · cited by 0
- Sym.coe_equivNatSumOfFintype_symm_applyproof · cited by 0
- Finsupp.mem_toMultisetproof · cited by 0