English
Let α be a nonunital, nonassociative semiring. For any finite M, N and functions v: M → α, B: Matrix M N α, and any column index j ∈ N with a column-replacing vector r: M → α, the product vecMul(v, B updated at column j by r) equals the update of vecMul(v, B) at index j by the scalar dotProduct(v, r).
Русский
Пусть α задана как полугруппа без единицы и без ассоциативности. При любых множества M, N и функциях v: M → α, B: матрица M×N над α, и фиксированном столбце j ∈ N с вектором r: M → α, получаемая матрица vecMul(v, B), после обновления j-го столбца на r, удовлетворяет равенству vecMul(v, B.updateCol(j, r)) = update(vecMul(v, B))_j( dotProduct(v, r) ).
LaTeX
$$$\\operatorname{vecMul}(v, B.updateCol(j, r)) = \\operatorname{update}(\\operatorname{vecMul}(v, B))\\, j\\; (\\langle v, r\\rangle).$$$
Lean4
theorem vecMul_updateCol [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) (B : Matrix m n α)
(j : n) (r : m → α) : v ᵥ* B.updateCol j r = Function.update (v ᵥ* B) j (v ⬝ᵥ r) :=
by
ext j'
obtain rfl | hj := eq_or_ne j' j
· simp [vecMul]
· simp [vecMul, hj]
