toMatrix_update — Mathlib

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]

Похожие утверждения