mathlib3

1f0f9813 - chore(linear_algebra/multilinear/basic): move finite-dimensionality to a new file (#14198)

chore(linear_algebra/multilinear/basic): move finite-dimensionality to a new file (#14198) `linear_algebra.matrix.to_lin` pulls in a lot of imports that appear to slow things down considerably in downstream files. The proof is moved without modification.