cons_dotProduct_cons — Mathlib

English

The dot product of vecCons x v with vecCons y w equals x y plus v dot w.

Русский

Скалярное произведение vecCons x v и vecCons y w равно x y плюс v ⬝ᵥ w.

LaTeX

$$$\\operatorname{dotProduct}(\\mathrm{vecCons}\\, x\\, v, \\mathrm{vecCons}\\, y\\, w) = x \\cdot y + v \\;\\classdot\\; w$$$

Lean4

theorem cons_dotProduct_cons (x : α) (v : Fin n → α) (y : α) (w : Fin n → α) :
    vecCons x v ⬝ᵥ vecCons y w = x * y + v ⬝ᵥ w := by simp

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