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

source

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

matrix.dot_product 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} {n : Type w} [semiring R] [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

source

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

v = w

source

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

(∀ (u : n → R), matrix.dot_product v u = matrix.dot_product w u) ↔ v = w

source

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

v = 0

source

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

(∀ (w : n → R), matrix.dot_product v w = 0) ↔ v = 0

source

@[simp]

theorem matrix.dot_product_self_eq_zero {R : Type v} {n : Type w} [fintype n] [linear_ordered_ring R] {v : n → R} :

matrix.dot_product v v = 0 ↔ v = 0

source

@[simp]

theorem matrix.dot_product_star_self_eq_zero {R : Type v} {n : Type w} [fintype n] [partial_order R] [non_unital_ring R] [star_ordered_ring R] [no_zero_divisors R] {v : n → R} :

matrix.dot_product (has_star.star v) v = 0 ↔ v = 0

Note that this applies to ℂ via complex.strict_ordered_comm_ring.

source

@[simp]

theorem matrix.dot_product_self_star_eq_zero {R : Type v} {n : Type w} [fintype n] [partial_order R] [non_unital_ring R] [star_ordered_ring R] [no_zero_divisors R] {v : n → R} :

matrix.dot_product v (has_star.star v) = 0 ↔ v = 0

Note that this applies to ℂ via complex.strict_ordered_comm_ring.