Commit 2020-05-19 17:00 607767e2

View on Github →

feat(algebra/big_operators): reversing an interval doesn't change the product (#2740) Also use Gauss summation in the Gauss summation formula. Inspired by #2688

Estimated changes

Modified src/algebra/big_operators.lean

added theorem finset.prod_Ico_reflect

added theorem finset.prod_range_reflect

added theorem finset.sum_Ico_reflect

added theorem finset.sum_range_reflect

Modified src/data/finset.lean

added theorem finset.Ico.image_const_sub

added theorem finset.range_image_pred_top_sub