Theorems · Theorem · combinatorics
Multiset.map_univ_coe
∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), Multiset.map (fun x => x.fst) Finset.univ.val = m- Defined in
- Mathlib.Data.Multiset.Fintype
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 84 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.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetproof · cited by 13,712
- Finset.univstatement and proof · cited by 3,473
- Multisetstatement and proof · cited by 2,627
- Multiset.mapstatement and proof · cited by 876
- Finset.valstatement and proof · cited by 438
- Multiset.countstatement · cited by 302
- Multiset.map_congrproof · cited by 232
- Multiset.map_mapproof · cited by 151
- Multiset.ToTypestatement and proof · cited by 30
- Multiset.toEnumFinsetproof · cited by 24
- Multiset.map_toEnumFinset_fstproof · cited by 7
- Multiset.coeEmbedding_applyproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- Multiset.prod_eq_prod_coeproof · cited by 1
- Multiset.map_univ_comp_coeproof · cited by 1
- Multiset.sum_eq_sum_coeproof · cited by 0