Commit 2025-11-04 09:08 0a5a3f89

feat(Mathlib/GroupTheory/Perm/MaximalSubgroups): maximal subgroups of the permutation group (#26457)

• Equiv.Perm.isCoatom_stabilizer: when s : Set α is not empty, nor its complementary subset, and if the cardinality of s is not half of that of α, then MulAction.stabilizer (Equiv.Perm α) s is a maximal subgroup of the symmetric group Equiv.Perm α. This is the intransitive case of the O'Nan-Scott classification.

TODO

• Appplication to primitivity of the action of Equiv.Perm α on finite combinations of α.
• Finish the classification