# Dot product of two vectors #

This file contains some results on the map Matrix.dotProduct, which maps two vectors v w : n → R to the sum of the entrywise products v i * w i.

## Main results #

• Matrix.dotProduct_stdBasis_one: the dot product of v with the ith standard basis vector is v i
• Matrix.dotProduct_eq_zero_iff: if v's' dot product with all w is zero, then v is zero

## Tags #

matrix, reindex

@[simp]
theorem Matrix.dotProduct_stdBasis_eq_mul {n : Type u_2} {R : Type u_4} [] [] [] (v : nR) (c : R) (i : n) :
Matrix.dotProduct v ((LinearMap.stdBasis R (fun (x : n) => R) i) c) = v i * c
theorem Matrix.dotProduct_stdBasis_one {n : Type u_2} {R : Type u_4} [] [] [] (v : nR) (i : n) :
Matrix.dotProduct v ((LinearMap.stdBasis R (fun (x : n) => R) i) 1) = v i
theorem Matrix.dotProduct_eq {n : Type u_2} {R : Type u_4} [] [] (v : nR) (w : nR) (h : ∀ (u : nR), ) :
v = w
theorem Matrix.dotProduct_eq_iff {n : Type u_2} {R : Type u_4} [] [] {v : nR} {w : nR} :
(∀ (u : nR), ) v = w
theorem Matrix.dotProduct_eq_zero {n : Type u_2} {R : Type u_4} [] [] (v : nR) (h : ∀ (w : nR), = 0) :
v = 0
theorem Matrix.dotProduct_eq_zero_iff {n : Type u_2} {R : Type u_4} [] [] {v : nR} :
(∀ (w : nR), = 0) v = 0
theorem Matrix.dotProduct_nonneg_of_nonneg {n : Type u_2} {R : Type u_4} [] [] {v : nR} {w : nR} (hv : 0 v) (hw : 0 w) :
0
theorem Matrix.dotProduct_le_dotProduct_of_nonneg_right {n : Type u_2} {R : Type u_4} [] [] {u : nR} {v : nR} {w : nR} (huv : u v) (hw : 0 w) :
theorem Matrix.dotProduct_le_dotProduct_of_nonneg_left {n : Type u_2} {R : Type u_4} [] [] {u : nR} {v : nR} {w : nR} (huv : u v) (hw : 0 w) :
@[simp]
theorem Matrix.dotProduct_self_eq_zero {n : Type u_2} {R : Type u_4} [] {v : nR} :
= 0 v = 0
@[simp]
theorem Matrix.dotProduct_star_self_eq_zero {n : Type u_2} {R : Type u_4} [] [] [] [] [] [] {v : nR} :
= 0 v = 0

Note that this applies to ℂ via Complex.strictOrderedCommRing.

@[simp]
theorem Matrix.dotProduct_self_star_eq_zero {n : Type u_2} {R : Type u_4} [] [] [] [] [] [] {v : nR} :
= 0 v = 0

Note that this applies to ℂ via Complex.strictOrderedCommRing.

@[simp]
theorem Matrix.conjTranspose_mul_self_eq_zero {m : Type u_1} {R : Type u_4} [] [] [] [] [] [] {n : Type u_5} {A : Matrix m n R} :
A.conjTranspose * A = 0 A = 0
@[simp]
theorem Matrix.self_mul_conjTranspose_eq_zero {n : Type u_2} {R : Type u_4} [] [] [] [] [] [] {m : Type u_5} {A : Matrix m n R} :
A * A.conjTranspose = 0 A = 0
theorem Matrix.conjTranspose_mul_self_mul_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [] [] [] [] [] [] [] {p : Type u_5} (A : Matrix m n R) (B : Matrix n p R) :
A.conjTranspose * A * B = 0 A * B = 0
theorem Matrix.self_mul_conjTranspose_mul_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [] [] [] [] [] [] [] {p : Type u_5} (A : Matrix m n R) (B : Matrix m p R) :
A * A.conjTranspose * B = 0 A.conjTranspose * B = 0
theorem Matrix.mul_self_mul_conjTranspose_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [] [] [] [] [] [] [] {p : Type u_5} (A : Matrix m n R) (B : Matrix p m R) :
B * (A * A.conjTranspose) = 0 B * A = 0
theorem Matrix.mul_conjTranspose_mul_self_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [] [] [] [] [] [] [] {p : Type u_5} (A : Matrix m n R) (B : Matrix p n R) :
B * (A.conjTranspose * A) = 0 B * A.conjTranspose = 0
theorem Matrix.conjTranspose_mul_self_mulVec_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [] [] [] [] [] [] [] (A : Matrix m n R) (v : nR) :
(A.conjTranspose * A).mulVec v = 0 A.mulVec v = 0
theorem Matrix.self_mul_conjTranspose_mulVec_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [] [] [] [] [] [] [] (A : Matrix m n R) (v : mR) :
(A * A.conjTranspose).mulVec v = 0 A.conjTranspose.mulVec v = 0
theorem Matrix.vecMul_conjTranspose_mul_self_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [] [] [] [] [] [] [] (A : Matrix m n R) (v : nR) :
Matrix.vecMul v (A.conjTranspose * A) = 0 Matrix.vecMul v A.conjTranspose = 0
theorem Matrix.vecMul_self_mul_conjTranspose_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [] [] [] [] [] [] [] (A : Matrix m n R) (v : mR) :
Matrix.vecMul v (A * A.conjTranspose) = 0 = 0