completion of a ring at an ideal

Stream: Is there code for X?

[Kevin Buzzard]

My post-doc @María Inés de Frutos Fernández is going to need $J$-adic completion of a commutative ring $R$ at an ideal (i.e. limit of R/J^n with its ring structure and topology). @Patrick Massot did this ever make it into mathlib, and if not then can Maria or I help to get it there?

[Patrick Massot]

The general theory of adic topology never went from the perfectoid project to mathlib, but I think Kenny PRed something independently.

[Patrick Massot]

docs#adic_completion

[Patrick Massot]

This is a completely ad hoc construction, without topology.