# mathlib3documentation

linear_algebra.matrix.dot_product

# Dot product of two vectors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[simp]
theorem matrix.dot_product_std_basis_eq_mul {R : Type v} {n : Type w} [semiring R] [fintype n] [decidable_eq n] (v : n R) (c : R) (i : n) :
( (λ (_x : n), R) i) c) = v i * c
@[simp]
theorem matrix.dot_product_std_basis_one {R : Type v} {n : Type w} [semiring R] [fintype n] [decidable_eq n] (v : n R) (i : n) :
( (λ (_x : n), R) i) 1) = v i
theorem matrix.dot_product_eq {R : Type v} {n : Type w} [semiring R] [fintype n] (v w : n R) (h : (u : n R), ) :
v = w
theorem matrix.dot_product_eq_iff {R : Type v} {n : Type w} [semiring R] [fintype n] {v w : n R} :
( (u : n R), v = w
theorem matrix.dot_product_eq_zero {R : Type v} {n : Type w} [semiring R] [fintype n] (v : n R) (h : (w : n R), = 0) :
v = 0
theorem matrix.dot_product_eq_zero_iff {R : Type v} {n : Type w} [semiring R] [fintype n] {v : n R} :
( (w : n R), = 0) v = 0
@[simp]
theorem matrix.dot_product_self_eq_zero {R : Type v} {n : Type w} [fintype n] {v : n R} :
= 0 v = 0
@[simp]
theorem matrix.dot_product_star_self_eq_zero {R : Type v} {n : Type w} [fintype n] {v : n R} :
= 0 v = 0

Note that this applies to ℂ via complex.strict_ordered_comm_ring.

@[simp]
theorem matrix.dot_product_self_star_eq_zero {R : Type v} {n : Type w} [fintype n] {v : n R} :
= 0 v = 0

Note that this applies to ℂ via complex.strict_ordered_comm_ring.