[Merged by Bors] - feat(topology/algebra/continuous_functions): algebra structure over continuous functions

[Nicknamen]

---

We proved topological-algebra-valued continuous functions have an algebra structure.

[semorrison]

Sorry it's taken a while for anyone to look at this --- the workshop on this week has been very distracting.

[semorrison]

These comments are only a superficial look; hopefully I'll be able to come back to this soon, or someone else will.

I wonder how hard just finishing off subsemiring will be. It would be good to get this mammoth refactor behind us. :-)

[Nicknamen]

In any case, I just copied the proofs of continuous functions being a group or a ring to also prove they are a module and an algebra! I am not sure many reviews are needed for this, but I added @PatrickMassot so that he can have a look as well! If he thinks this PR is ready to merge and we can merge it, I have a lot of other PRs in cue that I want to push, like the one has_continuous_mul

[semorrison]

I think this is fine. We'll let you get on with the other PRs. :-)

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests and docs