mathlib3

f191f521 - chore(algebra/big_operators): generalize `map_prod` to `monoid_hom_class` (#12354)

chore(algebra/big_operators): generalize `map_prod` to `monoid_hom_class` (#12354) This PR generalizes the following lemmas to `(add_)monoid_hom_class`: * `map_prod`, `map_sum` * `map_multiset_prod`, `map_multiset_sum` * `map_list_prod`, `map_list_sum` * `map_finsupp_prod`, `map_finsupp_sum` I haven't removed any of the existing specialized, namespaced versions of these lemmas yet, but I have marked them as `protected` and added a docstring saying to use the generic version instead. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>