mathlib3

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

#10253

Open