Commit 2023-01-28 21:25 287f7f54

View on Github →

feat: port Algebra.BigOperators.Intervals (#1901)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/BigOperators/Intervals.lean

added theorem Finset.prod_Ico_add'

added theorem Finset.prod_Ico_add

added theorem Finset.prod_Ico_consecutive

added theorem Finset.prod_Ico_div_bot

added theorem Finset.prod_Ico_eq_div

added theorem Finset.prod_Ico_eq_mul_inv

added theorem Finset.prod_Ico_id_eq_factorial

added theorem Finset.prod_Ico_reflect

added theorem Finset.prod_Ico_succ_div_top

added theorem Finset.prod_Ico_succ_top

added theorem Finset.prod_Ioc_consecutive

added theorem Finset.prod_Ioc_succ_top

added theorem Finset.prod_eq_prod_Ico_succ_bot

added theorem Finset.prod_ico_eq_prod_range

added theorem Finset.prod_range_add_one_eq_factorial

added theorem Finset.prod_range_mul_prod_Ico

added theorem Finset.prod_range_reflect

added theorem Finset.prod_range_sub_prod_range

added theorem Finset.prod_range_succ_div_prod

added theorem Finset.prod_range_succ_div_top

added theorem Finset.sum_Ico_Ico_comm

added theorem Finset.sum_Ico_by_parts

added theorem Finset.sum_Ico_reflect

added theorem Finset.sum_Ico_succ_top

added theorem Finset.sum_eq_sum_Ico_succ_bot

added theorem Finset.sum_range_by_parts

added theorem Finset.sum_range_id

added theorem Finset.sum_range_id_mul_two

added theorem Finset.sum_range_reflect