mathlib

7af5e86c - feat(algebra/big_operators/multiset): Multiset product under some usual maps (#10907)

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 `ℤ`).