Commit 2022-07-27 00:42 46b19752
View on Github →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.