English
Let b be a basis of ι → R on ι → R and A a matrix ι×ι. Then b.toMatrix (Pi.basisFun R ι) · A equals the matrix with entries (b.repr (A.col j))_i; i.e., the i-th row, j-th column equals the coordinate of A.col j in basis b.
Русский
Пусть b — база пространства, состоящего из функций ι → R, и A — матрица размером ι×ι. Тогда b.toMatrix (Pi.basisFun R ι) · A равна матрице, где элементы в i-й строке, j-м столбце равны координатам в базисе b вектора A.col j.
LaTeX
$$$b.toMatrix (\Pi\mathrm{basisFun} \; R \; ι) \cdot A = \mathrm{of}\; (i,j) \mapsto b.repr (A.col j)\, i$$$
Lean4
theorem basis_toMatrix_basisFun_mul (b : Basis ι R (ι → R)) (A : Matrix ι ι R) :
b.toMatrix (Pi.basisFun R ι) * A = of fun i j => b.repr (A.col j) i := by
classical
simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']
ext i j
rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply, Matrix.mulVec_single_one, Matrix.of_apply]
