Covering maps involving AddCircle

theorem AddCircle.isAddQuotientCoveringMap_coe {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] : IsAddQuotientCoveringMap QuotientAddGroup.mk ↥(AddSubgroup.zmultiples p)

theorem AddCircle.isCoveringMap_coe {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] : IsCoveringMap QuotientAddGroup.mk

theorem AddCircle.isLocalHomeomorph_coe {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] : IsLocalHomeomorph QuotientAddGroup.mk

theorem AddCircle.isAddQuotientCoveringMap_zsmul {𝕜 : Type u_1} [TopologicalSpace 𝕜] [Ring 𝕜] [IsTopologicalRing 𝕜] (p : 𝕜) [T0Space (AddCircle p)] {n : ℤ} (hn : IsUnit ↑n) : IsAddQuotientCoveringMap (fun (x : AddCircle p) => n • x) ↥(zsmulAddGroupHom n).ker

theorem AddCircle.isAddQuotientCoveringMap_nsmul {𝕜 : Type u_1} [TopologicalSpace 𝕜] [Ring 𝕜] [IsTopologicalRing 𝕜] (p : 𝕜) [T0Space (AddCircle p)] {n : ℕ} (hn : IsUnit ↑n) : IsAddQuotientCoveringMap (fun (x : AddCircle p) => n • x) ↥(nsmulAddMonoidHom n).ker

theorem AddCircle.isAddQuotientCoveringMap_zsmul_of_ne_zero {𝕜 : Type u_1} [TopologicalSpace 𝕜] [Ring 𝕜] [IsTopologicalRing 𝕜] (p : 𝕜) [T0Space (AddCircle p)] [Algebra ℚ 𝕜] (n : ℤ) [NeZero n] : IsAddQuotientCoveringMap (fun (x : AddCircle p) => n • x) ↥(zsmulAddGroupHom n).ker

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