Theorem Finset.sum_Ico_add_eq_sum_Ico_add_one

Modification history

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.sum_Ico_add_eq_sum_Ico_add_oneView on Github →