convergence of real-valued series

Stream: maths

[Jakub Kądziołka]

The undergraduate_todo page lists "Convergence of real-valued series". What exactly is meant there? It seems that this already exists and gets used often, e.g. docs#has_sum.tendsto_sum_nat

[Kevin Buzzard]

I think the issue here is that strictly speaking we only have absolute convergence (the lemma you link to isn't an iff)