mathlib

9f066f1f - refactor(linear_algebra/alternating): Use unapplied maps when possible (#5648)

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`