[Merged by Bors] - feat(group_theory/perm/sign): the alternating group

[awainverse]

Defines alternating_subgroup to be sign.ker
Proves a few basic lemmas about its cardinality

---

[eric-wieser]

This looks good to me now, thanks.

My only question would be whether we want to put this in its own file, perhaps group_theory/alternating, to make it easier to find.

[awainverse]

It would make more sense to me to split the sign.lean file into multiple files, because I think the support of a permutation, or the definition of disjoint permutations, has less to do with the sign homomorphism than the alternating group does. However, I realize most of the facts I want to show about the alternating group will actually land in the is_cycle file, so maybe it could make sense to split it off...

[eric-wieser]

bors d+

I pushed a golf of the card = 1 proof, along with the unique instance needed to prove it. Let's leave moving it to a new file for another time.

[bors]

✌️ awainverse can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[awainverse]

I've added one more small lemma, prod_list_swap_mem_alternating_subgroup_iff_even_length. Am I still good to merge this once CI builds, @eric-wieser ?

[eric-wieser]

bors d+ (again)

Let's wait for CI

[bors]

✌️ awainverse can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[awainverse]

Thanks!

[awainverse]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests