Commit 2026-09-09 11:47 a4c8ef0a

feat(GroupTheory/SpecificGroups/Cyclic): comparison of subgroups of a cyclic group (#40597) Add the following results about subgroup comparison in cyclic groups.

• IsCyclic.subgroup_le_iff_index_dvd: in a cyclic group, H ≤ K ↔ K.index ∣ H.index
• IsCyclic.subgroup_le_iff_card_dvd: if K is finite, H ≤ K ↔ Nat.card H ∣ Nat.card K
• IsCyclic.subgroup_eq_iff_card_eq: if H and K are finite, H = K ↔ Nat.card H = Nat.card K
• IsCyclic.infinite_of_ne_bot: a nontrivial subgroup of an infinite cyclic group is infinite Also add:
• Subgroup.exists_zpowers_eq_of_zpowers_eq_top: if g generates the group, every subgroup is of the form zpowers (g ^ i)
• Subgroup.index_eq_card_div: for H finite, H.index = Nat.card G / Nat.card H :robot: This PR was extracted from the SKW project by Claude.