Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-27 19:34 d57b6f9b

View on Github →

chore(data/dfinsupp): add yet more map_dfinsupp_sum lemmas (#8400) As always, the one of quadratically many combinations of FOO_hom.map_BAR_sum is never there when you need it.

Estimated changes

Modified src/data/dfinsupp.lean

added theorem add_equiv.map_dfinsupp_sum_add_hom

modified theorem add_monoid_hom.coe_dfinsupp_sum_add_hom

modified theorem add_monoid_hom.dfinsupp_sum_add_hom_apply

modified theorem add_monoid_hom.map_dfinsupp_sum_add_hom

modified theorem dfinsupp.prod_sum_index

added theorem mul_equiv.map_dfinsupp_prod

added theorem ring_hom.map_dfinsupp_prod

added theorem ring_hom.map_dfinsupp_sum

added theorem ring_hom.map_dfinsupp_sum_add_hom

Modified src/linear_algebra/basic.lean

added theorem linear_equiv.map_dfinsupp_sum

added theorem linear_equiv.map_dfinsupp_sum_add_hom

added theorem linear_equiv.map_finsupp_sum

added theorem linear_map.map_dfinsupp_sum_add_hom