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 #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.

[eric-wieser]

This will not build against master due to changes in fin. I pushed some changes to https://github.com/leanprover-community/mathlib/tree/exterior_algebra which make the necessary fixes, they might help you make the fixes here.

[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.