Theorems · Theorem · general topology

AddCircle.isAddQuotientCoveringMap_nsmul

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

Defined in

Mathlib.Topology.Covering.AddCircle

Cited by

1 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceRingIsTopologicalRingT0Space