Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-06 10:39 7af5e86c

View on Github →

feat(algebra/big_operators/multiset): Multiset product under some usual maps (#10907) Product of the image of a multiset under λ a, (f a)⁻¹, λ a, f a / g a, λ a, f a ^ n (for n in ℕ and ℤ).

Estimated changes

modified theorem finset.prod_inv_distrib
modified theorem multiset.pow_count
added theorem multiset.prod_hom'
added theorem multiset.prod_hom₂
added theorem multiset.prod_map_div
added theorem multiset.prod_map_inv'
modified theorem multiset.prod_map_mul
modified theorem multiset.prod_map_one
added theorem multiset.prod_map_pow
added theorem multiset.prod_map_zpow
added def div_monoid_hom
added def mul_monoid_hom
added def mul_mul_hom
added theorem list.foldl_hom₂
added theorem list.foldr_hom₂
modified theorem list.prod_hom_rel
added theorem list.prod_hom₂
added def smul_monoid_hom
added def smul_mul_hom