English
Let α be a NonUnitalCommSemiring. For A : m' → Fin n.succ → α and x ∈ α, v : Fin n → α, we have (of A) mulVec (vecCons x v) = x • vecHead ∘ A + (of (vecTail ∘ A)) mulVec v.
Русский
Пусть α — неунитная коммутативная полусемирия. Пусть A — матрица размера m'×(n+1) и x ∈ α, v ∈ α^n. Тогда (of A) умножить на vecCons x v равняется x умножить на первый столбец A плюс (of (vecTail A)) умножить на v.
LaTeX
$$$\big(\mathrm{of} A\big) \mulVec (\mathrm{vecCons}(x,v)) = x \cdot \vecHead \circ A + (\mathrm{of}(\vecTail \circ A)) \mulVec v.$$$
Lean4
@[simp]
theorem mulVec_cons {α} [NonUnitalCommSemiring α] (A : m' → Fin n.succ → α) (x : α) (v : Fin n → α) :
(of A) *ᵥ (vecCons x v) = x • vecHead ∘ A + (of (vecTail ∘ A)) *ᵥ v :=
by
ext i
simp [mulVec, mul_comm]
