mathlib3

31edca86 - chore(data/finsupp,data/dfinsupp,algebra/big_operators): add missing lemmas about sums of bundled functions (#5834)

chore(data/finsupp,data/dfinsupp,algebra/big_operators): add missing lemmas about sums of bundled functions (#5834) This adds missing lemmas about how `{finset,finsupp,dfinsupp}.{prod,sum}` acts on {coercion,application,evaluation} of `{add_monoid_hom,monoid_hom,linear_map}`. Specifically, it: * adds the lemmas: * `monoid_hom.coe_prod` * `monoid_hom.map_dfinsupp_prod` * `monoid_hom.dfinsupp_prod_apply` * `monoid_hom.finsupp_prod_apply` * `monoid_hom.coe_dfinsupp_prod` * `monoid_hom.coe_finsupp_prod` * that are the additive versions of the above for `add_monoid_hom`. * `linear_map.map_dfinsupp_sum` * `linear_map.dfinsupp_sum_apply` * `linear_map.finsupp_sum_apply` * `linear_map.coe_dfinsupp_sum` * `linear_map.coe_finsupp_sum` * Renames `linear_map.finsupp_sum` to `linear_map.map_finsupp_sum` for consistency with `linear_map.map_sum`. * Adds a new `monoid_hom.coe_fn` definition