Theorem Finset.mul_prod_Iio_eq_prod_Iic
Modification history
2025-05-04 00:34
Mathlib/Algebra/BigOperators/Intervals.lean
chore: Merge the two series of lemmas on big operators in locally finite orders (#17404) …
Modified Finset.mul_prod_Iio_eq_prod_IicView on Github →