Commit 2021-05-15 14:21 738c19f5

refactor(linear_algebra/matrix): split matrix.lean into multiple files (#7593) The file linear_algebra/matrix.lean used to be very big and contain a lot of parts that did not depend on each other, so I split each of those parts into its own little file. Most of the new files ended up in linear_algebra/matrix/, except for linear_algebra/trace.lean and linear_algebra/determinant.lean which did not contain anything matrix-specific. Apart from the local improvement in matrix.lean itself, the import graph is now also a bit cleaner. Renames:

• linear_algebra/determinant.lean -> linear_algebra/matrix/determinant.lean
• linear_algebra/nonsingular_inverse.lean -> linear_algebra/matrix/nonsingular_inverse.lean Split off from linear_algebra/matrix.lean:
• linear_algebra/matrix/basis.lean
• linear_algebra/matrix/block.lean
• linear_algebra/matrix/diagonal.lean
• linear_algebra/matrix/dot_product.lean
• linear_algebra/matrix/dual.lean
• linear_algebra/matrix/finite_dimensional.lean
• linear_algebra/matrix/reindex.lean
• linear_algebra/matrix/to_lin.lean
• linear_algebra/matrix/to_linear_equiv.lean
• linear_algebra/matrix/trace.lean
• linear_algebra/determinant.lean (Unfortunately, I could not persuade git to remember that I moved the original determinant.lean to matrix/determinant.lean)
• linear_algebra/trace.lean