mathlib

63427df9 - feat(group_theory/iwasawa.lean): add a proof of the Iwasawa criterion for simplicity

feat(group_theory/iwasawa.lean): add a proof of the Iwasawa criterion for simplicity Add the Iwasawa criterion for simplicity. This criterion can be used in the proof of simplicity of some classical groups such as the alternating group or the projective special linear group (these applications are TODO).