Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.dot_product_std_basis_one

Modification history

2021-05-15 14:21
src/linear_algebra/matrix.lean
refactor(linear_algebra/matrix): split matrix.lean into multiple files (#7593) …
Modified matrix.dot_product_std_basis_oneView on Github →
2021-01-27 08:41
src/linear_algebra/matrix.lean
feat(linear_algebra/matrix): A vector is zero iff its dot product with every vector is zero (#5837)
Added matrix.dot_product_std_basis_oneView on Github →