Theorem matrix.mul_minor_one
Modification history
2022-08-18 11:42
src/data/matrix/basic.lean
chore(data.matrix): rename `minor` to `submatrix` (#16101) …
Deleted matrix.mul_minor_oneView on Github →2022-04-25 05:10
src/data/matrix/basic.lean
chore(data/matrix): generalisation linter (#13655)
Modified matrix.mul_minor_oneView on Github →