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`.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

@@ -625,14 +625,18 @@ end CommGroup
 end IsSimpleGroup
 
 @[to_additive]
-theorem CommGroup.is_simple_iff_isCyclic_and_prime_card [Finite α] [CommGroup α] :
-    IsSimpleGroup α ↔ IsCyclic α ∧ (Nat.card α).Prime := by
-  constructor
-  · intro h
-    exact ⟨IsSimpleGroup.isCyclic, IsSimpleGroup.prime_card⟩
-  · rintro ⟨_, hp⟩
-    haveI : Fact (Nat.card α).Prime := ⟨hp⟩
-    exact isSimpleGroup_of_prime_card rfl
+theorem Group.is_simple_iff_prime_card [Finite α] [Group α] [IsMulCommutative α] :
+    IsSimpleGroup α ↔ (Nat.card α).Prime :=
+  ⟨fun h ↦ h.prime_card, fun h ↦ isSimpleGroup_of_prime_card (hp := ⟨h⟩) rfl⟩
+
+@[to_additive]
+theorem CommGroup.is_simple_iff_prime_card [Finite α] [CommGroup α] :
+    IsSimpleGroup α ↔ (Nat.card α).Prime :=
+  have : IsMulCommutative α := ⟨⟨mul_comm⟩⟩
+  Group.is_simple_iff_prime_card
+
+@[deprecated (since := "2025-11-19")]
+alias CommGroup.is_simple_iff_isCyclic_and_prime_card := CommGroup.is_simple_iff_prime_card
 
 section SpecificInstances
 
@@ -641,9 +645,8 @@ instance : IsAddCyclic ℤ := ⟨1, fun n ↦ ⟨n, by simp only [smul_eq_mul, m
 instance ZMod.instIsAddCyclic (n : ℕ) : IsAddCyclic (ZMod n) :=
   isAddCyclic_of_surjective (Int.castRingHom _) ZMod.intCast_surjective
 
-instance ZMod.instIsSimpleAddGroup {p : ℕ} [Fact p.Prime] : IsSimpleAddGroup (ZMod p) :=
-  AddCommGroup.is_simple_iff_isAddCyclic_and_prime_card.2
-    ⟨inferInstance, by simpa using (Fact.out : p.Prime)⟩
+instance ZMod.instIsSimpleAddGroup {p : ℕ} [hp : Fact p.Prime] : IsSimpleAddGroup (ZMod p) :=
+  AddCommGroup.is_simple_iff_prime_card.2 (by simpa using hp.out)
 
 end SpecificInstances