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

[kim-em]

This PR drops the (hS : ∃ a b : S, ¬ Commute a b) hypothesis from the schreier_conjecture eval problem, and records in the module docstring and the manifest notes why it is not needed. Schreier's conjecture is usually stated for non-abelian simple groups, but the form used here holds for every finite simple group: 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.

Reported by Boris Alexeev, who had already verified the abelian case in Lean, in "Formalized statement of CFSG?" https://leanprover.zulipchat.com/#narrow/channel/583339-AI-authored-projects/topic/Formalized.20statement.20of.20CFSG.3F/near/614674159

Confirmed independently against Mathlib before making the change, since dropping a hypothesis strengthens the statement and a false statement would make the problem unsolvable:

example (S : Type) [Group S] [Fintype S] [IsSimpleGroup S] (h : ∀ a b : S, Commute a b) :
    IsSolvable (MulAut S ⧸ (MulAut.conj : S →* MulAut S).range) := by
  let _ : CommGroup S := { (inferInstance : Group S) with mul_comm := h }
  have : IsCyclic S := IsSimpleGroup.isCyclic
  have : IsSolvable (MulAut S) :=
    solvable_of_surjective
      (f := (IsCyclic.mulAutMulEquiv S).symm.toMonoidHom) (MulEquiv.surjective _)
  infer_instance

schreier_conjecture is currently unsolved, so no accepted submission is invalidated. generated/ is left untouched, since CI regenerates it from source.

🤖 Prepared with Claude Code