mathlib documentation

linear_algebra.matrix.dot_product

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 #

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