Theorems · Theorem · combinatorics
Multiset.map_congr
∀ {α : Type u_1} {β : Type v} {f g : α → β} {s t : Multiset α},
s = t → (∀ x ∈ t, f x = g x) → Multiset.map f s = Multiset.map g t- Defined in
- Mathlib.Data.Multiset.MapFold
- Cited by
- 232 results in Mathlib
- Foundations
- Depth 15 from the axioms, rests on 81 definitions · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
Cited by232
Results whose statement or proof uses this declaration.
- UniqueFactorizationMonoid.prime_of_normalized_factorproof · cited by 23
- Polynomial.Splits.eq_prod_rootsproof · cited by 16
- Multiset.bind_congrproof · cited by 15
- Finset.noncommProd_congrproof · cited by 13
- UniqueFactorizationMonoid.normalizedFactors_mulproof · cited by 11
- Finset.fold_congrproof · cited by 11
- Polynomial.natDegree_sum_leproof · cited by 9
- UniqueFactorizationMonoid.normalize_normalized_factorproof · cited by 9
- Polynomial.splits_iff_exists_multisetproof · cited by 9
- UniqueFactorizationMonoid.normalizedFactors_oneproof · cited by 8
- Height.mulHeight_comp_equivproof · cited by 7
- UniqueFactorizationMonoid.factors_eq_normalizedFactorsproof · cited by 7
Showing the 200 most cited of 232.