Commit 2023-02-15 17:45 32253a1a

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.