Commit 2026-10-07 11:50 58d1b21e

View on Github →

chore(GroupTheory/Archimedean): spell cyclic results using IsCyclic (#43245) Replaces ∃ a, H = closure {a} with IsCyclic H, and some closure {a} with zpowers a.

Estimated changes

Modified Mathlib/GroupTheory/Archimedean.lean

deleted theorem Int.subgroup_cyclic

deleted theorem Subgroup.cyclic_of_isolated_one

deleted theorem Subgroup.cyclic_of_min

added theorem Subgroup.zpowers_eq_of_isLeast_mem_and_one_lt

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

added theorem Subgroup.isCyclic_of_disjoint_Ioo_one

deleted theorem Subgroup.mem_closure_singleton_iff_existsUnique_zpow

added theorem Subgroup.mem_zpowers_iff_existsUnique_zpow

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

added theorem Int.subgroup_cyclic

Modified Mathlib/NumberTheory/ModularForms/Cusps.lean

Modified Mathlib/Topology/Algebra/Order/Archimedean.lean

deleted theorem Subgroup.dense_iff_ne_zpowers

deleted theorem Subgroup.dense_or_cyclic

deleted theorem Subgroup.dense_xor_cyclic

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

added theorem Subgroup.dense_iff_not_isCyclic

added theorem Subgroup.dense_or_isCyclic

added theorem Subgroup.dense_xor_isCyclic

deleted theorem Subgroup.discrete_iff_cyclic

added theorem Subgroup.isCyclic_iff_discreteTopology

Modified Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean

Modified docs/undergrad.yaml