[Merged by Bors] - split(topology/algebra/infinite_sum): Split into four files

[YaelDillies]

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 feat(topology/algebra/infinite_sum): Multiplicativise #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 feat(topology/algebra/infinite_sum): Multiplicativise #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.

---

Partially requested by @eric-wieser

[eric-wieser]

• topology.algebra.big_operators.ring: Interaction of infinite sums and (scalar) multiplication. This cannot be multiplicativised.

mul_distrib_mul_action and mul_semiring_action are arguably counterexamples to this claim

[eric-wieser]

(I didn't request a split, only a reorder; but I'm not opposed either)

[YaelDillies]

• topology.algebra.big_operators.ring: Interaction of infinite sums and (scalar) multiplication. This cannot be multiplicativised.

mul_distrib_mul_action and mul_semiring_action are arguably counterexamples to this claim

Do you think this changes the way these files should be split? Note that it's not enough to have mul_distrib_mul_action and mul_semiring_action. We need ways to state they act continuously. I think has_continuous_const_smul provides this assumption for a few lemmas, but I doubt the other required one exists.

[eric-wieser]

This split generally looks reasonable to me. My main comments would be:

• infinite_sum might be preferable to big_operators as a name; it doesn't matter to me, but might to other reviewers
• topology.algebra.module.infinite_sum feels out of place now that the other file is not called infinite_sum.
• I'm not convinced about the placement of the smul lemmas, but that's minor.
• The docstrings of (some) of the new files could maybe do with a "main results" section.

[YaelDillies]

• I am reluctant to keeping infinite_sum as a name given that we're about to acquire infinite products in the same files. But I'd gladly take opinions
• Moved
• Moved
• I've expanded a bit for topology.algebra.big_operators.ring, but I have no idea about the other ones.

[eric-wieser]

bors d+

Thanks!

[bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

bors merge

[bors]

Build failed:

• Lint mathlib

[YaelDillies]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests