Discreteness of subgroups in archimedean ordered groups #
This file contains some supplements to the results in
Mathlib/Topology/Algebra/Order/Archimedean.lean, involving discreteness of subgroups, which
require heavier imports.
instance
Subgroup.instDiscreteTopologyZMultiples
{G : Type u_1}
[CommGroup G]
[LinearOrder G]
[IsOrderedMonoid G]
[TopologicalSpace G]
[OrderTopology G]
(g : G)
:
DiscreteTopology ↥(zpowers g)
In a linearly ordered group with the order topology, the powers of a single element form a discrete subgroup.
instance
AddSubgroup.instDiscreteTopologyZMultiples
{G : Type u_1}
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[TopologicalSpace G]
[OrderTopology G]
(g : G)
:
In a linearly ordered additive group with the order topology, the multiples of a single element form a discrete subgroup.
instance
Subgroup.instIsCyclicOfDiscreteTopology
{G : Type u_1}
[CommGroup G]
[LinearOrder G]
[IsOrderedMonoid G]
[TopologicalSpace G]
[OrderTopology G]
[MulArchimedean G]
[DiscreteTopology G]
:
IsCyclic G
instance
AddSubgroup.instIsAddCyclicOfDiscreteTopology
{G : Type u_1}
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[TopologicalSpace G]
[OrderTopology G]
[Archimedean G]
[DiscreteTopology G]
:
theorem
Subgroup.discrete_iff_cyclic
{G : Type u_1}
[CommGroup G]
[LinearOrder G]
[IsOrderedMonoid G]
[TopologicalSpace G]
[OrderTopology G]
[MulArchimedean G]
{H : Subgroup G}
:
In an Archimedean densely linearly ordered group (with the order topology), a subgroup is discrete iff it is cyclic.
theorem
AddSubgroup.discrete_iff_addCyclic
{G : Type u_1}
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[TopologicalSpace G]
[OrderTopology G]
[Archimedean G]
{H : AddSubgroup G}
:
In an Archimedean linearly ordered additive group (with the order topology), a subgroup is discrete iff it is cyclic.