A_n is simple iff n = 3 or 5 ≤ n

Stream: mathlib4

[Miyahara Kō]

I proved that A_n is simple iff n = 3 or 5 ≤ n in #23555.
The proof method is here: https://arbital.com/p/alternating_group_is_simple/
I'm now refactoring.

[Anatole Dedecker]

FYI: @Antoine Chambert-Loir proved this as a corollary of a much more powerful result, it hasn’t landed in Mathlib yet.

[Antoine Chambert-Loir]

To be fair, I now wonder what proof should land in mathlib…