dotProduct_cons — Mathlib

English

Analogous formula when the second argument is vecCons x w: dot product with v equals vecHead v times x plus tail interaction.

Русский

Аналогичная формула, когда второй аргумент — vecCons x w: скалярное произведение v с vecCons x w равно (голова v) умножить на x плюс скалярное произведение хвоста v и w.

LaTeX

$$$\\operatorname{dotProduct}(v, \\mathrm{vecCons}\\, x\\, w) = \\operatorname{vecHead} v \\cdot x + \\operatorname{dotProduct}(\\mathrm{vecTail}\\, v, w)$$$

Lean4

@[simp]
theorem dotProduct_cons (v : Fin n.succ → α) (x : α) (w : Fin n → α) :
    v ⬝ᵥ vecCons x w = vecHead v * x + vecTail v ⬝ᵥ w := by simp [dotProduct, Fin.sum_univ_succ, vecHead, vecTail]

Похожие утверждения