Theorems · Theorem · general topology

AddCircle.isAddQuotientCoveringMap_nsmul_of_ne_zero

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

Defined in

Mathlib.Topology.Covering.AddCircle

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceRingIsTopologicalRingT0SpaceAlgebraNeZero