IsAdic, IsAdicComplete and CompleteSpace

Stream: Is there code for X?

[Jiang Jiedong]

Hi everyone,
Do we have the relation between IsAdicComplete and CompleteSpace is mathlib? More precisely, do we have the following theorem?

• Let A be a topological ring, with the topology in A being I-adic for some ideal I (IsAdic I). Then A is complete as topological space (CompleteSpace A) if and only if A is I-adically complete (IsAdicComplete I A).

[Christian Merten]

I don't believe so @loogle IsAdicComplete, TopologicalSpace.

[loogle]

:exclamation: invalid field notation, identifier or numeral expected

[Christian Merten]

@loogle IsAdicComplete, TopologicalSpace

[loogle]

:shrug: nothing found

[Jiang Jiedong]

Thanks!