Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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`
- Loading branch information
1 parent
3c27e2e
commit 738c19f
Showing
32 changed files
with
2,381 additions
and
2,053 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.