Algebraic properties of dense vector dot products.

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.