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.

This is the full PR. I will instantly split it in smaller PR.

• depends on: [Merged by Bors] - Feat (GroupTheory/GroupAction/Hom/Pointwise) : generalize smul set lemmas to group actions #12023 generalization of pointwise lemmas for smul of sets.
• depends on: [Merged by Bors] - Feat (GroupTheory/GroupAction/Blocks) : blocks for a mul action #12049 blocks
• depends on: [Merged by Bors] - feat: primitive group actions #12052 primitive actions

the file also contains the content of the branches

• : [Merged by Bors] - feat(GroupTheory/GroupAction/Blocks): order iso between blocks and subgroups #13995 - order isomorphism between blocks containing a point and subgroups containing the stabilizer
• : [Merged by Bors] - feat(GroupTheory/GroupAction/Blocks): lemmas to handle blocks on finite sets #14029 - blocks (specific results for finite sets), Rubio theorem
• : [Merged by Bors] - feat: additivize equivariance of morphisms of actions #19171 - additivize equivariant morphisms