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 of v with the ith standard basis vector is v i
matrix.dot_product_eq_zero_iff: if v's' dot product with all w is zero, then v is zero

Tags #

matrix, reindex

source

@[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) :

v ⬝ᵥ ⇑(linear_map.std_basis R (λ (_x : n), R) i) c = (v i) * c

source

@[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) :

v ⬝ᵥ ⇑(linear_map.std_basis R (λ (_x : n), R) i) 1 = v i

source

theorem matrix.dot_product_eq {R : Type v} [semiring R] {n : Type w} [fintype n] (v w : n → R) (h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u) :

v = w

source

theorem matrix.dot_product_eq_iff {R : Type v} [semiring R] {n : Type w} [fintype n] {v w : n → R} :

(∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u) ↔ v = w

source

theorem matrix.dot_product_eq_zero {R : Type v} [semiring R] {n : Type w} [fintype n] (v : n → R) (h : ∀ (w : n → R), v ⬝ᵥ w = 0) :

v = 0

source

theorem matrix.dot_product_eq_zero_iff {R : Type v} [semiring R] {n : Type w} [fintype n] {v : n → R} :

(∀ (w : n → R), v ⬝ᵥ w = 0) ↔ v = 0