Commit 2021-01-08 14:20 9f066f1f

refactor(linear_algebra/alternating): Use unapplied maps when possible (#5648) Notably, this removes the need for a proof of map_add and map_smul in def alternatization, as the result is now already bundled with these proofs. This also:

• Replaces equiv.perm.sign p with p.sign for brevity
• Makes linear_map.comp_alternating_map an add_monoid_hom