mathlib

22e34370 - feat(algebra/big_operators/basic): lemmas prod_range_add, sum_range_add (#6484)