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_notMem_of_isAdicComplete_maximal {R : Type u_1} [CommRing R] (m : Ideal R) [hmax : m.IsMaximal] [IsAdicComplete m R] (r : R) : IsUnit r ↔ r ∉ m

@[deprecated isUnit_iff_notMem_of_isAdicComplete_maximal (since := "2025-05-24")]

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

Alias of isUnit_iff_notMem_of_isAdicComplete_maximal.

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