mathlib3

2cc8128f - feat(algebra/polynomial): generalize to `multiset` products (#7399)

feat(algebra/polynomial): generalize to `multiset` products (#7399) This PR generalizes the results in `algebra.polynomial.big_operators` to sums and products of multisets. The new multiset results are stated for `multiset.prod t`, not `(multiset.map t f).prod`. To get the latter, you can simply rewrite with `multiset.map_map`.