English
Let α be a nonunital nonassoc semiring. For a vector v ∈ α^{Fin n.succ}, a row vector w ∈ α^{o'→}, and B ∈ α^{Fin n → o' → α}, the product v ᵥ* of of(vecCons w B) equals vecHead v • w + vecMul (vecTail v) (of B).
Русский
Пусть α — неединичное неассоциативное полукольцо. Для v ∈ α^{Fin(n+1)}, w ∈ α^{o'}, B ∈ α^{Fin n → o' → α} произведение v ᵥ* (of(vecCons w B)) равно (голове v) умножить на w плюс vecMul (хвост v) на of B.
LaTeX
$$$\mathrm{vecMul}(\mathrm{vecHead}(v) \cdot w) + \mathrm{vecMul}(\mathrm{vecTail}(v), \mathrm{of}(B)).$$$
Lean4
@[simp]
theorem vecMul_cons (v : Fin n.succ → α) (w : o' → α) (B : Fin n → o' → α) :
v ᵥ* of (vecCons w B) = vecHead v • w + vecTail v ᵥ* of B :=
by
ext i
simp [vecMul]
