English
The jth column of the matrix representing f in bases v1, v2 is given by the coordinates of f(v1(j)) in the basis v2.
Русский
j-ый столбец матрицы, представляющей отображение f в базисах v1, v2, равен координатам образа f(v1(j)) в базисе v2.
LaTeX
$$$\\big(\\text{LinearMap.toMatrix } v_1 v_2 f\\big)_{i j} = v_2.repr\\big(f(v_1 j)\\big)_{i}$$$
Lean4
theorem toMatrix_apply (f : M₁ →ₗ[R] M₂) (i : m) (j : n) : LinearMap.toMatrix v₁ v₂ f i j = v₂.repr (f (v₁ j)) i :=
by
rw [LinearMap.toMatrix, LinearEquiv.trans_apply, LinearMap.toMatrix'_apply, LinearEquiv.arrowCongr_apply,
Basis.equivFun_symm_apply, Finset.sum_eq_single j, if_pos rfl, one_smul, Basis.equivFun_apply]
· intro j' _ hj'
rw [if_neg hj', zero_smul]
· intro hj
have := Finset.mem_univ j
contradiction
