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