Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-16 10:36 0f4d823c

View on Github →

feat(topology/algebra/uniform_ring): ring completions and algebra structures (#14841) If A is an algebra over a commutative ring R, so is the uniform_space.completion of A. If A is a normed algebra over a normed field 𝕜, then so is uniform_space.completion A.

Estimated changes