Fubini for infinite series

Stream: maths

[Filippo A. E. Nuccio]

Do we have Fubini's theorem for infinite series stating that we can exchange the order of doubly-indexed sequences under some absolute convergency assumption? We have docs#tsum_mul_tsum_of_summable_norm but this seems to apply only to "separable" series like

$$\sum_{m=0}^{\infty}\sum_{n=0}^{\infty}a_m\cdot b_n$$

whereas I need it for abitrary double-indexed series like

$$\sum_{m=0}^{\infty}\sum_{n=0}^{\infty}c_{m,n}=\sum_{m,n \in \mathbb{N}\times\mathbb{N}}c_{m,n}$$

[Heather Macbeth]

Maybe docs#has_sum.prod_fiberwise applied twice?

[Heather Macbeth]

Or docs#tsum_comm'

[Filippo A. E. Nuccio]

Oh nice! Thank you.

[Filippo A. E. Nuccio]

I guess that what confuses me is that some of the results concerning series are in topology.algebra.infinite_sum and some are in normed_space.