Commit 2021-03-17 10:17 4b1d5886

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.