Completion of a ring

Stream: Is there code for X?

[Juho Kupiainen]

https://en.wikipedia.org/wiki/Completion_of_a_ring

[Johan Commelin]

This was done during the perfectoid project in a very general context. I think it is in mathlib now: https://github.com/leanprover-community/mathlib/blob/1c4a2966ef25ec82e65337022a0764e87a81d992/src/topology/algebra/uniform_ring.lean#L59
Kudos to @Patrick Massot