Commit 2022-02-18 16:58 98643bca

View on Github →

feat(algebra/big_operators/intervals): summation by parts (#11814) Add the "summation by parts" identity over intervals of natural numbers, as well as some helper lemmas.

Estimated changes

Modified src/algebra/big_operators/intervals.lean

added theorem finset.prod_Ico_add'

added theorem finset.prod_Ico_div_bot

added theorem finset.prod_Ico_succ_div_top

added theorem finset.prod_range_succ_div_prod

added theorem finset.prod_range_succ_div_top

deleted theorem finset.sum_Ico_add

added theorem finset.sum_Ico_by_parts

added theorem finset.sum_range_by_parts