Commit 2021-05-07 04:59 efb283ca

View on Github →

feat(data/dfinsupp): add finset_sum_apply and coe_finset_sum (#7499) The names of the newadd_monoid_homs parallel the names in my recent quadratic_form PR, #7417.

Estimated changes

Modified src/data/dfinsupp.lean

added theorem dfinsupp.coe_finset_sum

added def dfinsupp.coe_fn_add_monoid_hom

added def dfinsupp.eval_add_monoid_hom

added theorem dfinsupp.finset_sum_apply