mathlib

49079c14 - feat(data/finsupp/basic): add `finset_sum_apply` and `coe_fn_add_hom` (#11423)

feat(data/finsupp/basic): add `finset_sum_apply` and `coe_fn_add_hom` (#11423) `finset_sum_apply`: Given a family of functions `f i : α → ℕ` indexed over `S : finset ι`, the sum of this family over `S` is a function `α → ℕ` whose value at `p : α` is `∑ (i : ι) in S, (f i) p` `coe_fn_add_monoid_hom`: Coercion from a `finsupp` to a function type is an `add_monoid_hom`. Proved by Alex J. Best Co-authored-by: Alex J. Best <alex.j.best@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>