refactor: drop the non-abelian hypothesis from Schreier's conjecture

LeanEval/GroupTheory/SchreierConjecture.lean

@@ -7,14 +7,19 @@ namespace GroupTheory
 /-!
 Schreier's conjecture (theorem, modulo CFSG).
 
-For every finite non-abelian simple group `S`, the outer automorphism group
+For every finite simple group `S`, the outer automorphism group
 `Out(S) := Aut(S) / Inn(S)` is solvable.
 
 This was conjectured by Schreier in the 1920s. It is verified case-by-case
 through the classification of finite simple groups: for each family
 (alternating, classical, exceptional Lie type, sporadic) one inspects `Out(S)`
 and observes solvability. No CFSG-free proof is known.
 
+Schreier's conjecture is usually stated for non-abelian `S`, but that
+hypothesis is unnecessary. A finite abelian simple group is `ZMod p`, so its
+inner automorphisms are trivial and `Out(S) ≅ Aut(S) ≅ (ZMod p)ˣ` is cyclic,
+hence solvable.
+
 `MulAut.conj : S →* MulAut S` sends `s ↦ (conjugation by s)`; its range is
 `Inn(S)`. The instance below records that `Inn(S)` is normal in `Aut(S)`,
 which is needed to form the quotient.
@@ -32,8 +37,7 @@ instance innNormal (S : Type*) [Group S] :
 
 @[eval_problem]
 theorem schreier_conjecture
-    (S : Type) [Group S] [Fintype S] [IsSimpleGroup S]
-    (hS : ∃ a b : S, ¬ Commute a b) :
+    (S : Type) [Group S] [Fintype S] [IsSimpleGroup S] :
     IsSolvable (MulAut S ⧸ (MulAut.conj : S →* MulAut S).range) := by
   sorry
 

manifests/problems/schreier_conjecture.toml

@@ -4,6 +4,6 @@ test = false
 module = "LeanEval.GroupTheory.SchreierConjecture"
 holes = ["schreier_conjecture"]
 submitter = "Kim Morrison"
-notes = "For every finite non-abelian simple group S, Out(S) := Aut(S)/Inn(S) is solvable. The statement requires the normality of Inn(S) ⊴ Aut(S), which is supplied by a local instance with a one-line proof (the conjugate of conj(s) by α equals conj(α(s))). Verified case-by-case via CFSG; no CFSG-free proof is known."
+notes = "For every finite simple group S, Out(S) := Aut(S)/Inn(S) is solvable. The statement requires the normality of Inn(S) ⊴ Aut(S), which is supplied by a local instance with a one-line proof (the conjugate of conj(s) by α equals conj(α(s))). Verified case-by-case via CFSG; no CFSG-free proof is known. Schreier's conjecture is usually stated for non-abelian S, but that hypothesis is unnecessary: a finite abelian simple group is ZMod p, whose inner automorphisms are trivial and whose automorphism group (ZMod p)ˣ is cyclic, hence solvable."
 source = "O. Schreier, Über die Erweiterung von Gruppen II, Abh. Math. Sem. Univ. Hamburg 4 (1926); CFSG, completed c. 2004."
-informal_solution = "Use the classification of finite simple groups. For each family — alternating Aₙ, classical Lie type, exceptional Lie type, sporadic — inspect the known Out(S) and verify it is solvable. For Aₙ (n ≥ 5, n ≠ 6), Out = ℤ/2; for A₆, Out = (ℤ/2)²; for groups of Lie type, Out is built from diagonal, field, and graph automorphisms (each step solvable); for sporadics, Out is trivial or ℤ/2."
+informal_solution = "Use the classification of finite simple groups. For each family — alternating Aₙ, classical Lie type, exceptional Lie type, sporadic — inspect the known Out(S) and verify it is solvable. For Aₙ (n ≥ 5, n ≠ 6), Out = ℤ/2; for A₆, Out = (ℤ/2)²; for groups of Lie type, Out is built from diagonal, field, and graph automorphisms (each step solvable); for sporadics, Out is trivial or ℤ/2. The abelian case needs no classification: S ≅ ZMod p, so Inn(S) is trivial and Out(S) ≅ (ZMod p)ˣ is cyclic."