∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Mul α] (u : m → α) (v : n → α) (j : n)
  (a : α), Matrix.vecMulVec u (Function.update v j a) = (Matrix.vecMulVec u v).updateCol j (MulOpposite.op a • u)