Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-27 08:41 61491ca3

View on Github →

feat(linear_algebra/matrix): A vector is zero iff its dot product with every vector is zero (#5837)

Estimated changes

Modified src/linear_algebra/matrix.lean

added theorem matrix.dot_product_eq

added theorem matrix.dot_product_eq_iff

added theorem matrix.dot_product_eq_zero

added theorem matrix.dot_product_eq_zero_iff

added theorem matrix.dot_product_std_basis_eq_mul

added theorem matrix.dot_product_std_basis_one