`multiplicative` (#15898)

Commit

3 years ago

feat(algebra/big_operators/basic): Sums and product in `additive`/`multiplicative` (#15898) and multiplicativizes `eq_sum_range_sub`.

Author

YaelDillies

Parents