mathlib

46b19752 - refactor(algebra/big_operators/basic): Use `to_additive` (#15702)

refactor(algebra/big_operators/basic): Use `to_additive` (#15702) Prove `sum_range_sub` and `sum_range_sub'` using `to_additive`. Change the statement of `prod_range_div` to use `f (i + 1) / f i` rather than `f (i + 1) * (f i)⁻¹`. Rename `sum_range_sub_of_monotone` to `sum_range_tsub`.