mathlib3
efb283ca - feat(data/dfinsupp): add `finset_sum_apply` and `coe_finset_sum` (#7499)

Commit

5 years ago

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

Author

eric-wieser

Parents

9acbe588

mathlib3 efb283ca - feat(data/dfinsupp): add `finset_sum_apply` and `coe_finset_sum` (#7499)

mathlib3
efb283ca - feat(data/dfinsupp): add `finset_sum_apply` and `coe_finset_sum` (#7499)