Dot product of two vectors #
This file contains some results on the map matrix.dot_product, which maps two
vectors v w : n → R to the sum of the entrywise products v i * w i.
Main results #
matrix.dot_product_std_basis_one: the dot product ofvwith theith standard basis vector isv imatrix.dot_product_eq_zero_iff: ifv's' dot product with allwis zero, thenvis zero
Tags #
matrix, reindex
@[simp]
theorem
matrix.dot_product_std_basis_eq_mul
{R : Type v}
[semiring R]
{n : Type w}
[fintype n]
[decidable_eq n]
(v : n → R)
(c : R)
(i : n) :
matrix.dot_product v (⇑(linear_map.std_basis R (λ (_x : n), R) i) c) = v i * c
@[simp]
theorem
matrix.dot_product_std_basis_one
{R : Type v}
[semiring R]
{n : Type w}
[fintype n]
[decidable_eq n]
(v : n → R)
(i : n) :
matrix.dot_product v (⇑(linear_map.std_basis R (λ (_x : n), R) i) 1) = v i
theorem
matrix.dot_product_eq
{R : Type v}
[semiring R]
{n : Type w}
[fintype n]
(v w : n → R)
(h : ∀ (u : n → R), matrix.dot_product v u = matrix.dot_product w u) :
v = w
theorem
matrix.dot_product_eq_iff
{R : Type v}
[semiring R]
{n : Type w}
[fintype n]
{v w : n → R} :
(∀ (u : n → R), matrix.dot_product v u = matrix.dot_product w u) ↔ v = w
theorem
matrix.dot_product_eq_zero
{R : Type v}
[semiring R]
{n : Type w}
[fintype n]
(v : n → R)
(h : ∀ (w : n → R), matrix.dot_product v w = 0) :
v = 0
theorem
matrix.dot_product_eq_zero_iff
{R : Type v}
[semiring R]
{n : Type w}
[fintype n]
{v : n → R} :
(∀ (w : n → R), matrix.dot_product v w = 0) ↔ v = 0