feat(group/perm/sign): swap_adj_induction_on

[zhangir-azerbayev]

1. Defines the multilinear map that sends a tuple of elements of an algebra to their product.
2. Defines the typeclass alternating_map that extends multilinear_map. Superseded by [Merged by Bors] - feat(linear_algebra): Add alternating multilinear maps #5102
3. Proves some lemmas about permutations and lists that are necessary for (1) and (2), and some lemmas about permutations of fin n that will be useful for formalizing exterior algebras.

---

This PR is essentially a number of lemmas and constructions I wrote for the exterior_algebra branch stated at the appropriate level of generality.

A particular area where I could use some help is deciding where long proofs should be split into several shorter lemmas.

[semorrison]

This is quite a complicated statement. Would it be easier to say that there a list of nats, such that equiv.swap i j is the product of the corresponding adjacent transpositions?

[semorrison]

Also, it might be easier if you split this into several lemmas: prove the first one with the hypothesis that i < j.

[zhangir-azerbayev]

If I were to state the lemma using a list of nats, I can't think of a good way of keeping track of an l.1 + 1 < n for each l ∈ L.

[semorrison]

You could, e.g. have i j : fin (n+1), then produce in one declaration a list (fin n), and then in a second declaration equiv.swap i j = (L.map ...).prod, where the ... converts a fin n into the adjacent transposition of fin (n+1).

I'm not saying this is essential, just potentially results in cleaner statements, and proofs split into smaller chunks.

[eric-wieser]

I suspect the now-merged #4316 contains some pieces and lemma names that can be reused and copied here

[eric-wieser]

I went ahead and fixed the merge conflicts, and removed all the proofs that now exist elsewhere in mathlib.

[eric-wieser]

I've renamed this PR, since all the algebra pieces have been merged elsewhere.