Topic: completion of uniform spaces
Patrick Massot (Jun 25 2018 at 19:08):
The perfectoid projects crucially needs completions of topological rings. I can see mathlib already has a lot about completion of uniform spaces but I also remember the definition of real numbers was changed by @Mario Carneiro. Is there anything we should know before doing completions of topological rings?
Mario Carneiro (Jun 26 2018 at 00:16):
All the material for completion of topological rings via uniform completion is still there. It simply isn't being used to construct the reals anymore, since the direct construction is better in a number of other ways. If you have need for a generic completion operator in a more abstract context, feel free to use it
Last updated: May 18 2021 at 06:15 UTC