Theorems · Theorem · combinatorics
Multiset.map_toEnumFinset_fst
∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), Multiset.map Prod.fst m.toEnumFinset.val = m- Defined in
- Mathlib.Data.Multiset.Fintype
- Cited by
- 7 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.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Multisetstatement and proof · cited by 2,627
- Multiset.mapstatement · cited by 876
- Finset.valstatement and proof · cited by 438
- Multiset.cardproof · cited by 375
- Multiset.countproof · cited by 302
- Multiset.card_mapproof · cited by 57
- Multiset.ext'proof · cited by 31
- Multiset.rangeproof · cited by 30
- Multiset.toEnumFinsetstatement and proof · cited by 24
- Multiset.filter_congrproof · cited by 11
- Finset.singleton_productproof · cited by 8
- Multiset.card_rangeproof · cited by 5
Cited by7
Results whose statement or proof uses this declaration.
- Multiset.map_univ_coeproof · cited by 3
- Multiset.card_toEnumFinsetproof · cited by 3
- AlgebraicClosure.toSplittingField_coeffproof · cited by 1
- Multiset.toEnumFinset_subset_iffproof · cited by 0
- Multiset.sum_eq_sum_toEnumFinsetproof · cited by 0
- Multiset.prod_eq_prod_toEnumFinsetproof · cited by 0
- Multiset.image_toEnumFinset_fstproof · cited by 0