Theorem matrix.rank_vec_mul_vec
Modification history
2023-04-09 07:51
src/linear_algebra/free_module/finite/matrix.lean
refactor(linear_algebra/matrix/finite_dimensional): deduplicate (#18770) …
Modified matrix.rank_vec_mul_vecView on Github →2023-04-08 20:46
src/linear_algebra/matrix/to_lin.lean
chore(linear_algebra/dimension): tidy lemma names for `linear_map.rank` (#18769) …
Modified matrix.rank_vec_mul_vecView on Github →2021-08-26 13:06
src/linear_algebra/matrix/to_lin.lean
feat(*): remove the `fintype` requirement from matrices. (#8810) …
Modified matrix.rank_vec_mul_vecView on Github →2021-05-15 14:21
src/linear_algebra/matrix.lean
refactor(linear_algebra/matrix): split matrix.lean into multiple files (#7593) …
Modified matrix.rank_vec_mul_vecView on Github →2020-10-05 11:38
src/linear_algebra/matrix.lean
refactor(linear_algebra/matrix): consistent naming (#4345) …
Modified matrix.rank_vec_mul_vecView on Github →2020-08-20 21:33
src/linear_algebra/matrix.lean
chore(data/matrix, linear_algebra): generalize universe parameters (#3879) …
Modified matrix.rank_vec_mul_vecView on Github →2020-04-07 03:42
src/linear_algebra/matrix.lean
chore(algebra/big_operators): drop some `decidable_eq` assumptions (#2332) …
Modified matrix.rank_vec_mul_vecView on Github →