English
Let DecidableEq m and Mul α hold. For u: m → α, v: n → α and j ∈ n, a ∈ α, updating the j-th column of v multiplies the corresponding column of vecMulVec by the scalar on the left, yielding the updated vecMulVec.
Русский
Пусть существует декидируемость и умножение. Пусть u: m→α, v: n→α и j∈n, a∈α. Обновление j-го столбца в v приводит к тому, что vecMulVec обновляется в соответствующем столбце на a • u слева.
LaTeX
$$$\\operatorname{vecMulVec}(u, \\operatorname{update}(v,j,a)) = (\\operatorname{vecMulVec}(u,v)).updateCol(j, (\\operatorname{MulOpposite}.op a) \\cdot u).$$$
Lean4
theorem vecMulVec_update [DecidableEq n] [Mul α] (u : m → α) (v : n → α) (j : n) (a : α) :
vecMulVec u (Function.update v j a) = (vecMulVec u v).updateCol j (MulOpposite.op a • u) :=
by
ext i j'
obtain rfl | hi := eq_or_ne j' j
· simp [vecMulVec_apply]
· simp [vecMulVec_apply, hi]
