mathlib

c8651967 - feat(src/group_theory/specific_groups/alternating.lean): prove that the alternating group is perfect

feat(src/group_theory/specific_groups/alternating.lean): prove that the alternating group is perfect Prove what is said: the alternating group on α, with 5 ≤ fintype.card α, is perfect, aka equal to its commutator subgroup. Prove two intermediate lemmas, that 3-cycles are commutators and are contained in the commutator subgroup Prove two ugly lemmas that should be (and certainly will) golfed by people more competent than me.