Commit 2022-01-14 17:47 49079c14
View on Github →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