Commit 2021-01-27 08:41 31edca86
View on Github →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
tolinear_map.map_finsupp_sum
for consistency withlinear_map.map_sum
. - Adds a new
monoid_hom.coe_fn
definition