mathlib

d6241cb0 - feat(linear_algebra/*): Use alternating maps for wedge and determinant (#5124)

feat(linear_algebra/*): Use alternating maps for wedge and determinant (#5124) This : * Adds `exterior_algebra.ι_multi`, where `ι_multi ![a, b ,c]` = `ι a * ι b * ι c` * Makes `det_row_multilinear` an `alternating_map` * Makes `is_basis.det` an `alternating_map`