mathlib

b4ac6fdf - refactor(linear_algebra/alternating): Use unapplied maps when possible

refactor(linear_algebra/alternating): Use unapplied maps when possible 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.