Complete Implies Quasi-Complete

A complete Noetherian local ring is quasi-complete (Anderson, 2014, Theorem 3).

theorem krull_intersection_sup {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (J : Ideal R) : ⨅ (n : ℕ), J ⊔ IsLocalRing.maximalIdeal R ^ n = J

theorem comap_map_algebraMap_adicCompletion {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] (I : Ideal R) : have M := IsLocalRing.maximalIdeal R; Ideal.comap (algebraMap R (AdicCompletion M R)) (Ideal.map (algebraMap R (AdicCompletion M R)) I) = I

theorem anderson_complete_isQuasiComplete (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (hR : IsAdicComplete (IsLocalRing.maximalIdeal R) R) : IsQuasiComplete R