Commit 2025-11-20 09:36 7ce54af0

refactor(GroupTheory/SpecificGroups/Cyclic): clean up statement of classification of abelian finite simple groups (#31829) This PR changes the statement of the classification of abelian finite simple groups from

IsSimpleGroup α ↔ IsCyclic α ∧ (Nat.card α).Prime

to

IsSimpleGroup α ↔ (Nat.card α).Prime

since IsCyclic α is implied by (Nat.card α).Prime.