Commit 2024-10-04 04:46 6dd0053d

View on Github →

feat: Big operators indexed by an interval (#17280) From LeanCamCombi

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean

added theorem Finset.left_mul_prod_Ioc

added theorem Finset.left_mul_prod_Ioi

added theorem Finset.left_mul_prod_Ioo

added theorem Finset.prod_Ico_mul_right

added theorem Finset.prod_Iio_mul_right

added theorem Finset.prod_Ioc_mul_left

added theorem Finset.prod_Ioi_mul_left

added theorem Finset.prod_Ioo_mul_left

added theorem Finset.prod_Ioo_mul_right

added theorem Finset.right_mul_prod_Ico

added theorem Finset.right_mul_prod_Iio

added theorem Finset.right_mul_prod_Ioo