mathlib3

a199f856 - feat(topology/uniform_space): Abstract completions (#1374)

feat(topology/uniform_space): Abstract completions (#1374) * feat(topology/uniform_space): Abstract completions Define abstract completions, study their properties and derived constructions. Use this study in the concrete completion files, and for comparing completions constructed at different level of generality, especially for real numbers. This comes from the perfectoid spaces project. * Apply suggestions from code review by Johan Co-Authored-By: Johan Commelin <johan@commelin.net> * Fix build. When I created the PR, github complained it couldn't automatically merge, and I was not careful enough when I merged... * chore(topology/uniform_space): rename completion_pkg * fix(compare_reals): create namespace * Fix build