mathlib

e55d470c - feat(specific_groups/alternating_group): The alternating group on 5 elements is simple (#7502)

feat(specific_groups/alternating_group): The alternating group on 5 elements is simple (#7502) Shows that `is_simple_group (alternating_group (fin 5))` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>