Commit 2024-01-10 14:23 f8ed0192

View on Github →

feat: Products over finite intervals (#9386) From LeanCamCombi

Estimated changes

Modified Mathlib/Algebra/BigOperators/Intervals.lean

added theorem Finset.mul_prod_Ico_eq_prod_Icc

added theorem Finset.mul_prod_Iio_eq_prod_Iic

added theorem Finset.mul_prod_Ioc_eq_prod_Icc

added theorem Finset.mul_prod_Ioi_eq_prod_Ici

modified theorem Finset.prod_Ico_consecutive

modified theorem Finset.prod_Ico_eq_prod_range

added theorem Finset.prod_Ico_mul_eq_prod_Icc

modified theorem Finset.prod_Ico_reflect

modified theorem Finset.prod_Ico_succ_top

added theorem Finset.prod_Iio_mul_eq_prod_Iic

modified theorem Finset.prod_Ioc_consecutive

added theorem Finset.prod_Ioc_mul_eq_prod_Icc

modified theorem Finset.prod_Ioc_succ_top

added theorem Finset.prod_Ioi_mul_eq_prod_Ici

modified theorem Finset.prod_eq_prod_Ico_succ_bot

modified theorem Finset.prod_range_mul_prod_Ico

modified theorem Finset.prod_range_reflect