Documentation

Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

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.

source
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.

source
instance AddSubgroup.instDiscreteTopologyZMultiples {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] (g : G) :
DiscreteTopology ↥(zmultiples g)

In a linearly ordered additive group with the order topology, the multiples of a single element form a discrete subgroup.

source
instance Subgroup.instIsCyclicOfDiscreteTopology {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [DiscreteTopology G] :
IsCyclic G
source
instance AddSubgroup.instIsAddCyclicOfDiscreteTopology {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] [DiscreteTopology G] :
IsAddCyclic G
source
theorem Subgroup.dense_or_isCyclic {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] (H : Subgroup G) :
Dense ↑H ∨ IsCyclic ↥H

A subgroup of an archimedean linear ordered multiplicative commutative group G with order topology either is dense in G or is a cyclic subgroup.

source
theorem AddSubgroup.dense_or_isCyclic {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] (H : AddSubgroup G) :
Dense ↑H ∨ IsAddCyclic ↥H

An additive subgroup of an archimedean linear ordered additive commutative group G with order topology either is dense in G or is a cyclic subgroup.

source
@[deprecated Subgroup.dense_or_isCyclic (since := "2026-08-30")]
theorem Subgroup.dense_or_cyclic {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] (H : Subgroup G) :
Dense ↑H ∨ IsCyclic ↥H

Alias of Subgroup.dense_or_isCyclic.

A subgroup of an archimedean linear ordered multiplicative commutative group G with order topology either is dense in G or is a cyclic subgroup.

source
@[deprecated AddSubgroup.dense_or_isCyclic (since := "2026-08-30")]
theorem AddSubgroup.dense_or_cyclic {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] (H : AddSubgroup G) :
Dense ↑H ∨ IsAddCyclic ↥H

Alias of AddSubgroup.dense_or_isCyclic.

An additive subgroup of an archimedean linear ordered additive commutative group G with order topology either is dense in G or is a cyclic subgroup.

source
theorem Subgroup.dense_xor_isCyclic {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] (H : Subgroup G) :
Xor (Dense ↑H) (IsCyclic ↥H)

In a nontrivial densely linear ordered archimedean topological multiplicative group, a subgroup is either dense or is cyclic, but not both.

For a non-exclusive Or version with weaker assumptions, see Subgroup.dense_or_cyclic above.

source
theorem AddSubgroup.dense_xor_isAddCyclic {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] [Nontrivial G] [DenselyOrdered G] (H : AddSubgroup G) :
Xor (Dense ↑H) (IsAddCyclic ↥H)

In a nontrivial densely linear ordered archimedean topological additive group, a subgroup is either dense or is cyclic, but not both.

For a non-exclusive Or version with weaker assumptions, see AddSubgroup.dense_or_cyclic above.

source
@[deprecated Subgroup.dense_xor_isCyclic (since := "2026-08-30")]
theorem Subgroup.dense_xor_cyclic {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] (H : Subgroup G) :
Xor (Dense ↑H) (IsCyclic ↥H)

Alias of Subgroup.dense_xor_isCyclic.

In a nontrivial densely linear ordered archimedean topological multiplicative group, a subgroup is either dense or is cyclic, but not both.

For a non-exclusive Or version with weaker assumptions, see Subgroup.dense_or_cyclic above.

source
@[deprecated AddSubgroup.dense_xor_isAddCyclic (since := "2026-08-30")]
theorem AddSubgroup.dense_xor_cyclic {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] [Nontrivial G] [DenselyOrdered G] (H : AddSubgroup G) :
Xor (Dense ↑H) (IsAddCyclic ↥H)

Alias of AddSubgroup.dense_xor_isAddCyclic.

In a nontrivial densely linear ordered archimedean topological additive group, a subgroup is either dense or is cyclic, but not both.

For a non-exclusive Or version with weaker assumptions, see AddSubgroup.dense_or_cyclic above.

source
@[deprecated Subgroup.dense_xor_isCyclic (since := "2026-04-27")]
theorem Subgroup.dense_xor'_cyclic {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] (H : Subgroup G) :
Xor (Dense ↑H) (IsCyclic ↥H)

Alias of Subgroup.dense_xor_isCyclic.

In a nontrivial densely linear ordered archimedean topological multiplicative group, a subgroup is either dense or is cyclic, but not both.

For a non-exclusive Or version with weaker assumptions, see Subgroup.dense_or_cyclic above.

source
@[deprecated AddSubgroup.dense_xor_isAddCyclic (since := "2026-04-27")]
theorem AddSubgroup.dense_xor'_addCyclic {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] [Nontrivial G] [DenselyOrdered G] (H : AddSubgroup G) :
Xor (Dense ↑H) (IsAddCyclic ↥H)

Alias of AddSubgroup.dense_xor_isAddCyclic.

In a nontrivial densely linear ordered archimedean topological additive group, a subgroup is either dense or is cyclic, but not both.

For a non-exclusive Or version with weaker assumptions, see AddSubgroup.dense_or_cyclic above.

source
theorem Subgroup.dense_iff_not_isCyclic {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] {H : Subgroup G} :
Dense ↑H ↔ ¬IsCyclic ↥H
source
theorem AddSubgroup.dense_iff_not_isAddCyclic {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] [Nontrivial G] [DenselyOrdered G] {H : AddSubgroup G} :
Dense ↑H ↔ ¬IsAddCyclic ↥H
source
@[deprecated Subgroup.dense_iff_not_isCyclic (since := "2026-08-30")]
theorem Subgroup.dense_iff_ne_zpowers {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] {H : Subgroup G} :
Dense ↑H ↔ ¬IsCyclic ↥H

Alias of Subgroup.dense_iff_not_isCyclic.

source
@[deprecated AddSubgroup.dense_iff_not_isAddCyclic (since := "2026-08-30")]
theorem AddSubgroup.dense_iff_ne_zmultiples {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] [Nontrivial G] [DenselyOrdered G] {H : AddSubgroup G} :
Dense ↑H ↔ ¬IsAddCyclic ↥H

Alias of AddSubgroup.dense_iff_not_isAddCyclic.

source
theorem Subgroup.isCyclic_iff_discreteTopology {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] {H : Subgroup G} :
IsCyclic ↥H ↔ DiscreteTopology ↥H

In an Archimedean linearly ordered group (with the order topology), a subgroup is discrete iff it is cyclic.

source
theorem AddSubgroup.isAddCyclic_iff_discreteTopology {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] {H : AddSubgroup G} :
IsAddCyclic ↥H ↔ DiscreteTopology ↥H

In an Archimedean linearly ordered additive group (with the order topology), a subgroup is discrete iff it is cyclic.

source
@[deprecated Subgroup.isCyclic_iff_discreteTopology (since := "2026-08-30")]
theorem Subgroup.discrete_iff_cyclic {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] {H : Subgroup G} :
IsCyclic ↥H ↔ DiscreteTopology ↥H

Alias of Subgroup.isCyclic_iff_discreteTopology.

In an Archimedean linearly ordered group (with the order topology), a subgroup is discrete iff it is cyclic.

source
@[deprecated AddSubgroup.isAddCyclic_iff_discreteTopology (since := "2026-08-30")]
theorem AddSubgroup.discrete_iff_addCyclic {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] {H : AddSubgroup G} :
IsAddCyclic ↥H ↔ DiscreteTopology ↥H

Alias of AddSubgroup.isAddCyclic_iff_discreteTopology.

In an Archimedean linearly ordered additive group (with the order topology), a subgroup is discrete iff it is cyclic.