basic): add `finsupp.prod_congr` and `sum_congr` (#10568)

Commit

4 years ago

feat(data/finsupp/basic): add `finsupp.prod_congr` and `sum_congr` (#10568) These are the counterparts for `finsupp` of a simpler form of `finset.prod_congr`

Author

stuart-presnell

Parents

42d3cbc3

mathlib ac767452 - feat(data/finsupp/basic): add `finsupp.prod_congr` and `sum_congr` (#10568)

mathlib
ac767452 - feat(data/finsupp/basic): add `finsupp.prod_congr` and `sum_congr` (#10568)