English
Let DecidableEq m and Mul α hold. For u: m → α, v: n → α, i ∈ m and a ∈ α, the row-wise product vecMulVec after updating the i-th entry of u to a equals the i-th row of vecMulVec u v updated by a times v.
Русский
Пусть существуют пространство векторов над кольцом α и операция умножения. Пусть u: M→α и v: N→α; тогда обновление координаты i в u на a приводит к тому, что vecMulVec (обновлённый u) v имеет i-ую строку равную (a • v) вместо старой i-ой строки.
LaTeX
$$$\\operatorname{vecMulVec}(\\operatorname{update}(u,i,a), v) = (\\operatorname{vecMulVec}(u,v)).updateRow(i, a \\cdot v).$$$
Lean4
theorem update_vecMulVec [DecidableEq m] [Mul α] (u : m → α) (v : n → α) (i : m) (a : α) :
vecMulVec (Function.update u i a) v = (vecMulVec u v).updateRow i (a • v) :=
by
ext i' j
obtain rfl | hi := eq_or_ne i' i
· simp [vecMulVec_apply]
· simp [vecMulVec_apply, hi]
