Stream: Is there code for X?
Topic: Completion of a ring
Juho Kupiainen (Dec 22 2019 at 14:10):
Johan Commelin (Dec 23 2019 at 15:38):
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
Last updated: May 07 2021 at 19:12 UTC