English
Let α be a nonunital nonassoc semiring. For v : Fin m → α, A : Fin k → n' → α, w : n' → α with Fintype n', one has (of ∘ vecCons v A) mulVec w = vecCons (dotProduct v w) ((of A) mulVec w).
Русский
Пусть α — неединичное неассоциативное полукольцо. Пусть v и A задают матрицу через vecCons, тогда произведение (of ∘ vecCons v A) на w равно состоятелному вектору, первый компонент которого — dotProduct(v,w), а остальные — (of A) mulVec w.
LaTeX
$$$\big( \mathrm{of} \circ \mathrm{vecCons}(v,A) \big) \mulVec w = \mathrm{vecCons}(\mathrm{dotProduct}(v,w)) (\mathrm{of} A \mulVec w).$$$
Lean4
@[simp]
theorem cons_mulVec [Fintype n'] (v : n' → α) (A : Fin m → n' → α) (w : n' → α) :
(of <| vecCons v A) *ᵥ w = vecCons (v ⬝ᵥ w) (of A *ᵥ w) :=
by
ext i
refine Fin.cases ?_ ?_ i <;> simp [mulVec]
