Simplicity of alternating groups

Stream: mathlib4

[Stepan Nesterov]

Was there a previous attempt to prove that $A_n$ is a simple group for $n \ge 5$ in Mathlib (e.g. is this a PR somewhere)?
If not, I would be happy to claim the task.

[Bryan Wang]

Maybe #mathlib4 > (Another) proof of alternating group A_n is simple?

[Stepan Nesterov]

So a bunch of people have proofs locally, but no PR to mathlib was made?

[Vlad Tsyrklevich]

There’s an open PR, you can find it by searching for “alternating” in the mathlib PRs

[Filippo A. E. Nuccio]

@Antoine Chambert-Loir

[Michael Rothgang]

There are in fact at least two mathlib PRs about this, #26051 and #33082. (This answers the question above, sorry.)

[Miyahara Kō]

#26051 is my PR, but since #33082 is more refined, I plan to split off the defs and lemmas from #26051 that were useful for my proofs, and then close it.

[Snir Broshi]

(btw $n = 5$ already exists, docs#alternatingGroup.isSimpleGroup_five)

[Antoine Chambert-Loir]

Indeed. Once the general proof I proposed is merged (and if it is), I will write a PR that moves the initial proof for $n=5$ to the archive.

[Antoine Chambert-Loir]

unless this is @Miyahara Kō that is merged—as far as I understand, it builds on the proof for $n=5$.