English
Updating the vector v at position j corresponds to updating the j-th column of the matrix e.toMatrix v by the coordinates of the update in basis e.
Русский
Обновление вектора v на позиции j эквивалентно обновлению j-го столбца матрицы e.toMatrix v координатами обновления в базисе e.
LaTeX
$$e.toMatrix(Function.update v j x) = Matrix.updateCol (e.toMatrix v) j (e.repr x)$$
Lean4
theorem toMatrix_update [DecidableEq ι'] (x : M) :
e.toMatrix (Function.update v j x) = Matrix.updateCol (e.toMatrix v) j (e.repr x) :=
by
ext i' k
rw [Basis.toMatrix, Matrix.updateCol_apply, e.toMatrix_apply]
split_ifs with h
· rw [h, update_self j x v]
· rw [update_of_ne h]