Basic Properties of Complete Local Ring

In this file we prove that a ring that is adic complete with respect to a maximal ideal ia a local ring (complete local ring).

theorem isUnit_iff_nmem_of_isAdicComplete_maximal {R : Type u_1} [CommRing R] (m : Ideal R) [hmax : m.IsMaximal] [IsAdicComplete m R] (r : R) : IsUnit r ↔ r ∉ m

theorem isLocalRing_of_isAdicComplete_maximal {R : Type u_1} [CommRing R] (m : Ideal R) [hmax : m.IsMaximal] [IsAdicComplete m R] : IsLocalRing R