cons_vecMul_cons — Mathlib

English

Let α be a nonunital nonassoc semiring. For A : m' → Fin n.succ → α, x ∈ α, v ∈ α^n, we have vecMul (vecCons x v) (of (vecCons w B)) equals x • w + vecMul v (of B).

Русский

Пусть α — неединичное неассоциативное полукольцо. Пусть A — матрица размера m' × (n+1) с элементами α, x ∈ α, v ∈ α^n. Тогда произведение vecMul (vecCons x v) (of (vecCons w B)) равно x • w + vecMul v (of B).

LaTeX

$$$\mathrm{vecMul}(\mathrm{vecCons}(x,v),\mathrm{of}(\mathrm{vecCons}(w,B))) = x \cdot w + \mathrm{vecMul}(v,\mathrm{of}(B)).$$$

Lean4

theorem cons_vecMul_cons (x : α) (v : Fin n → α) (w : o' → α) (B : Fin n → o' → α) :
    vecCons x v ᵥ* of (vecCons w B) = x • w + v ᵥ* of B := by simp

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