basic): add two versions of `finsupp.mul_prod_erase` (#10708)

Commit

4 years ago

feat(data/finsupp/basic): add two versions of `finsupp.mul_prod_erase` (#10708) Adding a counterpart for `finsupp` of `finset.mul_prod_erase`

Author

stuart-presnell

Parents