feat(topology/algebra/uniform_ring): ring completions and algebra structures

[mariainesdff]

If A is an algebra over R, so is the uniform_space.completion of A.

---

• [x] depends on: #14846

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#14846~~ By Dependent Issues (🤖). Happy coding!

[jcommelin]

Sorry for being very late with this comment: I think it would be nice if all the theory were developed for an arbitrary abstract_completion package, and then specialised in a few lines to uniform_space.completion.

I understand that this (math-free) generalization would be quite some work. At least it would be good to record it as a TODO.

[mariainesdff]

Sorry for being very late with this comment: I think it would be nice if all the theory were developed for an arbitrary abstract_completion package, and then specialised in a few lines to uniform_space.completion.

I understand that this (math-free) generalization would be quite some work. At least it would be good to record it as a TODO.

What do you exactly mean by this? I've seen docs#topology.uniform_space.abstract_completion, but I'm not sure what you would like to add. In any case, I would rather leave this as a TODO for now, I would like to close this PR and #14249 before going on vacation, if possible.

[ocfnash]

I suggest addressing @jcommelin 's remark by adding a sentence along the lines of:

TODO Generalise the results here from the concrete `completion` to any `abstract_completion`.

to the doc string of the three files changed.

I note you have also addressed all other comments. Thus:

bors d+

[bors[bot]]

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

[eric-wieser]

Can you update the PR description to mention the normed_algebra instance too? (And anything else you think is interesting that was added in review)

[mariainesdff]

bors r+

[bors[bot]]

Build failed (retrying...):

• Build mathlib

[bors[bot]]

Build failed (retrying...):

• Build mathlib

[bors[bot]]

Build failed (retrying...):

• Build mathlib
• Lint mathlib
• Run tests

[mariainesdff]

bors r+

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

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