Theorems · Theorem · combinatorics
Multiset.pmap_eq_map
∀ {α : Type u_1} {β : Type v} (p : α → Prop) (f : α → β) (s : Multiset α) (H : ∀ a ∈ s, p a),
Multiset.pmap (fun a x => f a) s H = Multiset.map f s- Defined in
- Mathlib.Data.Multiset.MapFold
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- Multiset.pmapstatement · cited by 16
Cited by7
Results whose statement or proof uses this declaration.
- Associates.map_subtype_coe_factors'proof · cited by 3
- Multiset.map_eq_map_of_bij_of_nodupproof · cited by 3
- PrimeMultiset.to_ofNatMultisetproof · cited by 2
- PrimeMultiset.to_ofPNatMultisetproof · cited by 2
- Polynomial.Splits.of_splits_map_of_injectiveproof · cited by 1
- Finset.map_val_val_powersetCardproof · cited by 1
- Multiset.extract_gcdproof · cited by 0