mathlib

4b1d5886 - chore(linear_algebra/determinant): redefine det using multilinear_map.alternatization (#6708)

chore(linear_algebra/determinant): redefine det using multilinear_map.alternatization (#6708) This slightly changes the definitional unfolding of `matrix.det` (moving a function application outside a sum and adjusting the version of int-multiplication used). By doing this, a large number of proofs become a trivial application of a more general statement about alternating maps. `det_row_multilinear` already existed prior to this commit, but now `det` is defined in terms of it instead of the other way around. We still need both, as otherwise we would break `M.det` dot notation, as `det_row_multilinear` does not have its argument expressed as a matrix.