Commit 2020-05-13 12:20 9f16f866

feat(topology/algebra/infinite_sum): sums on subtypes (#2659) For f a summable function defined on the integers, we prove the formula

(∑ i in range k, f i) + (∑' i, f (i + k)) = (∑' i, f i)

This is deduced from a general version on subtypes of the form univ - s where s is a finset.