basic): Sum over a product of finsets, right version (#10124)

Commit

4 years ago

feat(algebra/big_operators/basic): Sum over a product of finsets, right version (#10124) This adds `finset.sum_prod_right` and renames `finset.sum_prod` to `finset.sum_prod_left`.

Author

YaelDillies

Parents

ca5c4b37

mathlib3 bf068540 - feat(algebra/big_operators/basic): Sum over a product of finsets, right version (#10124)

mathlib3
bf068540 - feat(algebra/big_operators/basic): Sum over a product of finsets, right version (#10124)