English
For a matrix M ∈ Mat_{n×n}(R) and a vector v ∈ M1, the result of applying the linear map Matrix.toLinAlgEquiv v1 M to v is the sum over j of the j-th coordinate of M written in the v1-coordinates times the basis vector v1_j.
Русский
Для матрицы M и вектора v линейное отображение Matrix.toLinAlgEquiv v1 M возвращает сумма по j координат M в базисе v1, умноженная на вектор v1_j.
LaTeX
$$$\mathrm{toLinAlgEquiv}_{v_1}(M)(v) = \sum_j \big( M *^v v_1.repr v \big)_j \; v_{1,j}$$$
Lean4
theorem toLinAlgEquiv_apply (M : Matrix n n R) (v : M₁) :
Matrix.toLinAlgEquiv v₁ M v = ∑ j, (M *ᵥ v₁.repr v) j • v₁ j :=
show v₁.equivFun.symm (Matrix.toLinAlgEquiv' M (v₁.repr v)) = _ by
rw [Matrix.toLinAlgEquiv'_apply, v₁.equivFun_symm_apply]
