multiset): rename `prod_le_sum_prod` to `prod_le_prod_map` (#16420)

Commit

3 years ago

fix(algebra/big_operators/multiset): rename `prod_le_sum_prod` to `prod_le_prod_map` (#16420)

Author

astrainfinita

Parents