English
Define the dot product of two finite-index functions v and w with values in a ring as the sum of entrywise products: dotProduct(v,w) = sum over i of v(i)·w(i).
Русский
Определим скалярное произведение двух функций v и w с конечной индексацией как сумму попарных произведений: dotProduct(v,w) = суммa по i от v(i)·w(i).
LaTeX
$$$$\operatorname{dotProduct}(v,w) = \sum_{i} v(i) \cdot w(i) \quad (v,w: m \to \alpha)$$$$
Lean4
/-- `dotProduct v w` is the sum of the entrywise products `v i * w i`.
See also `dotProductEquiv`. -/
def dotProduct [Mul α] [AddCommMonoid α] (v w : m → α) : α :=
∑ i, v i * w i
