cons_dotProduct — Mathlib

English

The dot product of vecCons x v with w equals vecHead v times x plus the dot product of v with vecTail w.

Русский

Скалярное произведение vecCons x v и w равно (голова v) умножить на x плюс скалярное произведение v и vecTail w.

LaTeX

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

Lean4

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

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