Commit 2025-12-29 09:01 f65bc60c

feat(GroupTheory): add Subgroup.le_zpowers_iff (#33125) Adds an instance:

instance Subgroup.isCyclic_zpowers [Group G] (g : G) : IsCyclic (Subgroup.zpowers g)

and a lemma characterizing the subgroups of a cyclic subgroup:

theorem Subgroup.le_zpowers_iff (g : G) (H : Subgroup G) : 
    H ≤ Subgroup.zpowers g ↔ ∃ n : ℕ, H = Subgroup.zpowers (g ^ n)