theorem
AddCircle.isAddQuotientCoveringMap_coe
{𝕜 : Type u_1}
[AddCommGroup 𝕜]
(p : 𝕜)
[TopologicalSpace 𝕜]
[IsTopologicalAddGroup 𝕜]
[DiscreteTopology ↥(AddSubgroup.zmultiples p)]
:
theorem
AddCircle.isCoveringMap_coe
{𝕜 : Type u_1}
[AddCommGroup 𝕜]
(p : 𝕜)
[TopologicalSpace 𝕜]
[IsTopologicalAddGroup 𝕜]
[DiscreteTopology ↥(AddSubgroup.zmultiples p)]
:
theorem
AddCircle.isLocalHomeomorph_coe
{𝕜 : Type u_1}
[AddCommGroup 𝕜]
(p : 𝕜)
[TopologicalSpace 𝕜]
[IsTopologicalAddGroup 𝕜]
[DiscreteTopology ↥(AddSubgroup.zmultiples p)]
:
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