Rearrangements of an absolutely convergent series have the same sum

Statement

Let $\sum a_n$ be a real series that converges absolutely, with sum $A$. Let $\sigma \colon \mathbb{N} \to \mathbb{N}$ be a bijection. Then the rearrangement $\sum a_{\sigma(n)}$ converges absolutely, and its sum is $A$.

Remarks

Given $\varepsilon > 0$, choose $N$ with $\sum_{n > N} |a_n| < \varepsilon$. For large $m$, the first $m$ terms of the rearrangement include $a_0, \dots, a_N$. So the two partial sums differ by less than $\varepsilon$. By the Riemann rearrangement theorem, the converse also holds for real series. Mathlib states a general form for sums over a type, as Equiv.tsum_eq.

Explanations

L1 human

When the series converges absolutely, the far terms have a small total size, whatever their order. So a new order changes the partial sums only by a small amount.