Theorems · Theorem · group theory
Multiset.prod_hom
∀ {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] (s : Multiset M) {F : Type u_8}
[inst_2 : FunLike F M N] [MonoidHomClass F M N] (f : F), (Multiset.map (⇑f) s).prod = f s.prod- Cited by
- 8 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- Multisetstatement and proof · cited by 2,627
- FunLikestatement and proof · cited by 2,560
- CommMonoidstatement and proof · cited by 2,264
- Multiset.mapstatement · cited by 876
- Multiset.prodstatement · cited by 528
- MonoidHomClassstatement and proof · cited by 244
- List.prod_homproof · cited by 8
Cited by8
Results whose statement or proof uses this declaration.
- map_multiset_prodproof · cited by 21
- MonoidHom.map_multiset_prodproof · cited by 12
- Multiset.prod_hom'proof · cited by 4
- MulEquiv.uniqueFactorizationMonoidproof · cited by 3
- Polynomial.map_multiset_prodproof · cited by 2
- Multiset.prod_map_inv'proof · cited by 1
- MvPolynomial.rename_msymmproof · cited by 1
- Multiset.prod_map_zpowproof · cited by 1