mathlib

32253a1a - split(topology/algebra/infinite_sum): Split into four files (#18414)

split(topology/algebra/infinite_sum): Split into four files (#18414) Over the past five years, `topology.algebra.infinite_sum` has grown pretty big. This PR splits off a third of it to three new files. Precisely, split `topology.algebra.infinite_sum` into: * `topology.algebra.infinite_sum.basic`: Definitions and theory in monoids. All this will be multiplicativised in #18405. * `topology.algebra.infinite_sum.ring`: Interaction of infinite sums and (scalar) multiplication. This mostly cannot be multiplicativised. * `topology.algebra.infinite_sum.order`: Interaction of infinite sums and order. Most of this will be multiplicativised in #18405. Incidentally, this brings down some files' imports by quite a lot. Also move the `star` and `mul_opposite` material to the end of the file to facilitate multiplicativisation in #18405. Johannes wrote some of all these files, except `topology.algebra.infinite_sum.real` whose first lemma I could trace back as coming from #753, with the others coming from #1739.