Commit 2020-12-15 01:31 b364d337

chore(topology/instances/ennreal): remove summability assumption in tendsto_sum_nat_add (#5366) We have currently

lemma tendsto_sum_nat_add (f : ℕ → ℝ≥0) (hf : summable f) : tendsto (λ i, ∑' k, f (k + i)) at_top (𝓝 0)

However, the summability assumption is not necessary as otherwise all sums are zero, and the statement still holds. The PR removes the assumption.