mathlib

b364d337 - chore(topology/instances/ennreal): remove summability assumption in tendsto_sum_nat_add (#5366)

chore(topology/instances/ennreal): remove summability assumption in tendsto_sum_nat_add (#5366) We have currently ```lean 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.