Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.mul_vec_one

Modification history

2023-04-21 14:26
src/data/matrix/basic.lean
feat(data/matrix/basic): miscellaneous defs and lemmas (#8289) …
Added matrix.mul_vec_oneView on Github →
2021-07-16 00:27
src/data/matrix/basic.lean
chore(data/matrix/basic): add lemmas about dot_product and mul_vec (#8325) …
Deleted matrix.mul_vec_oneView on Github →
2020-02-08 10:42
src/data/matrix/basic.lean
feat(linear_algebra): The Special linear group SL(n, R) (#1960) …
Added matrix.mul_vec_oneView on Github →