Theorem Finset.prod_eq_prod_Ico_succ_bot

Modification history

2025-07-05 03:31
Mathlib/Algebra/BigOperators/Intervals.lean
chore(Algebra/BigOperators): rename variables away from greek letters (#26521) …
Deleted Finset.prod_eq_prod_Ico_succ_botView on Github →
2025-05-04 00:34
Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean
chore: Merge the two series of lemmas on big operators in locally finite orders (#17404) …
Added Finset.prod_eq_prod_Ico_succ_botView on Github →
2024-01-10 14:23
Mathlib/Algebra/BigOperators/Intervals.lean
feat: Products over finite intervals (#9386) …
Modified Finset.prod_eq_prod_Ico_succ_botView on Github →
2023-01-28 21:25
Mathlib/Algebra/BigOperators/Intervals.lean
feat: port Algebra.BigOperators.Intervals (#1901)
Added Finset.prod_eq_prod_Ico_succ_botView on Github →