Connection between adic properties and topological properties

Main results

• IsAdic.isPrecomplete_iff: IsPrecomplete I R is equivalent to CompleteSpace R in the adic topology.

theorem IsAdic.isPrecomplete_iff {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] {I : Ideal R} (hI : IsAdic I) : IsPrecomplete I R ↔ CompleteSpace R

IsPrecomplete I R is equivalent to being complete in the adic topology.