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
isLocalRing_of_isAdicComplete_maximal
{R : Type u_1}
[CommRing R]
(m : Ideal R)
[m.IsMaximal]
[IsAdicComplete m R]
: