mathlib

008205aa - chore(analysis/normed/field/basic): split (#18195)

chore(analysis/normed/field/basic): split (#18195) Split material on infinite sums out of `analysis/normed/field/basic` into a new file `/infinite_sum`. This mimics the structure of `analysis/normed/group/*`, and reduces the imports of the former.