∀ {𝕜 : Type u_1} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [IsTopologicalRing 𝕜] (p : 𝕜) [T0Space (AddCircle p)]
  {n : ℕ}, IsUnit ↑n → IsAddQuotientCoveringMap (fun x => n • x) ↥(nsmulAddMonoidHom n).ker