alternating.lean): remove ugly lemmas

Commit

4 years ago

style(src/group_theory/specific_groups/alternating.lean): remove ugly lemmas Shorten the proof of `alternating_group_is_perfect` using a simplification by Johan Commelin

References

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

Author

Antoine Chambert-Loir

Parents

1157ed05

mathlib3 d1ca2d4c - style(src/group_theory/specific_groups/alternating.lean): remove ugly lemmas

mathlib3
d1ca2d4c - style(src/group_theory/specific_groups/alternating.lean): remove ugly lemmas