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