theorem Vector.dotProduct_ofFn {R : Type u} [Mul R] [Add R] [OfNat R 0] {n : Nat} (f g : Fin n → R) : (ofFn f).dotProduct (ofFn g) = List.foldl (fun (acc : R) (i : Fin n) => acc + f i * g i) 0 (List.finRange n)

A dot product of two ofFn vectors is the List.finRange fold of their pointwise products. The reference dotProduct reduction that keeps ofFn-built rows and columns visible to the fold-algebra lemmas.

theorem Vector.dotProduct_extendZero {R : Type u} [Lean.Grind.Ring R] (m d : Nat) (F G : Fin m → R) : (ofFn fun (i : Fin (m + d)) => if h : ↑i < m then F ⟨↑i, h⟩ else 0).dotProduct (ofFn fun (i : Fin (m + d)) => if h : ↑i < m then G ⟨↑i, h⟩ else 0) = (ofFn F).dotProduct (ofFn G)

Zero-extending two vectors on the right (to a common larger length m + d) leaves their dot product unchanged: every added term is 0 * _ or _ * 0. This is the vector-level engine behind the matrix padding lemma.

theorem Vector.dotProduct_add_left {n : Nat} {R : Type u} [Lean.Grind.Ring R] (u v w : Vector R n) : (u + v).dotProduct w = u.dotProduct w + v.dotProduct w

Dot product is additive in its left argument.

theorem Vector.dotProduct_smul_left {n : Nat} {R : Type u} [Lean.Grind.Ring R] (c : R) (u w : Vector R n) : (c • u).dotProduct w = c * u.dotProduct w

Dot product is homogeneous in its left argument.

theorem Vector.dotProduct_comm {n : Nat} {R : Type u} [Lean.Grind.CommRing R] (u v : Vector R n) : u.dotProduct v = v.dotProduct u

Dot product is symmetric over a commutative coefficient type.

theorem Vector.dotProduct_add_right {n : Nat} {R : Type u} [Lean.Grind.Ring R] (u v w : Vector R n) : u.dotProduct (v + w) = u.dotProduct v + u.dotProduct w

Dot product is additive in its right argument.

theorem Vector.dotProduct_smul_right {n : Nat} {R : Type u} [Lean.Grind.CommRing R] (c : R) (u v : Vector R n) : u.dotProduct (c • v) = c * u.dotProduct v

Dot product is homogeneous in its right argument.

theorem Vector.dotProduct_sub_left {n : Nat} {R : Type u} [Lean.Grind.Ring R] (u v w : Vector R n) : (u - v).dotProduct w = u.dotProduct w - v.dotProduct w

Dot product is additive over subtraction in its left argument.

theorem Vector.dotProduct_sub_right {n : Nat} {R : Type u} [Lean.Grind.Ring R] (u v w : Vector R n) : u.dotProduct (v - w) = u.dotProduct v - u.dotProduct w

Dot product is additive over subtraction in its right argument.

theorem Vector.dotProduct_sub_smul_left {n : Nat} {R : Type u} [Lean.Grind.Ring R] (u v w : Vector R n) (c : R) : (u - c • v).dotProduct w = u.dotProduct w - c * v.dotProduct w

Dot product distributes over subtracting a scalar multiple in the left argument.

theorem Vector.dotProduct_sub_smul_right {n : Nat} {R : Type u} [Lean.Grind.CommRing R] (u v w : Vector R n) (c : R) : u.dotProduct (v - c • w) = u.dotProduct v - c * u.dotProduct w

Dot product distributes over subtracting a scalar multiple in the right argument.

theorem Vector.dotProduct_append {R : Type u} [Lean.Grind.Ring R] {p q : Nat} (u : Vector R p) (v : Vector R q) (x : Vector R p) (y : Vector R q) : (u ++ v).dotProduct (x ++ y) = u.dotProduct x + v.dotProduct y

Splitting a dot product along a sum-shaped dimension: the dot product of two concatenated vectors is the sum of the dot products of the halves. This is the vector-level decomposition behind the 2×2 block product of matrices.