Commit 2025-10-28 21:32 b6ac07d4

View on Github →

feat(Topology/Algebra/Order/Archimedean): subgroups cyclic iff discrete (#30471) An add subgroup of the reals (or similar groups) is discrete iff it's cyclic, and related statements.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

added theorem LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered

added theorem LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem zpowers_mabs

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

added theorem LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int

added theorem LinearOrderedCommGroup.isCyclic_iff_nonempty_equiv_int

Created Mathlib/Topology/Algebra/Order/ArchimedeanDiscrete.lean

added theorem Subgroup.discrete_iff_cyclic