feat(GroupTheory/GroupAction/Iwasawa): the Iwasawa criterion for simplicity (#12048)

The Iwasawa criterion for simplicity

• IwasawaStructure : the structure underlying the Iwasawa criterion For a group G, this consists of an action of G on a type α and, for every a : α, of a subgroup T a, such that the following properties hold:
  • for all a, T a is commutative
  • for all g : G and a : α, T (g • a) = MulAut.conj g • T a
  • the subgroups T a generate G We then prove two versions of the Iwasawa criterion when there is an Iwasawa structure.
• IwasawaStructure.commutator_le asserts that if the action of G on α is quasiprimitive, then every normal subgroup that acts nontrivially contains commutator G
• IwasawaStructure.isSimpleGroup : the Iwasawa criterion for simplicity If the action of G on α is quasiprimitive and faithful, and G is nontrivial and perfect, then G is simple.