Zulip Chat Archive

Stream: Is there code for X?

Topic: Completion of a ring

view this post on Zulip Juho Kupiainen (Dec 22 2019 at 14:10):


view this post on Zulip 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