English
For bases b1,b2,b3 and a matrix A, the matrix of the linear map corresponding to A with respect to b1,b2,b3 equals A times the matrix connecting b2 to b3; more precisely, A · b1.toMatrix b2 = LinearMap.toMatrix b2 b3 (toLin b1 b3 A).
Русский
Для базисов b1,b2,b3 и матрицы A матрица линейного отображения, соответствующего A, относительно b1,b2,b3 равна A, умноженной на матрицу перехода от b2 к b3: A · b1.toMatrix b2 = LinearMap.toMatrix b2 b3 (toLin b1 b3 A).
LaTeX
$$$A \cdot b_1.toMatrix b_2 = \mathrm{ToMatrix}_{b_2,b_3}(\mathrm{toLin}_{b_1,b_3}(A))$$$
Lean4
theorem mul_basis_toMatrix [DecidableEq ι] [DecidableEq ι'] (b₁ : Basis ι R M) (b₂ : Basis ι' R M) (b₃ : Basis κ R N)
(A : Matrix κ ι R) : A * b₁.toMatrix b₂ = LinearMap.toMatrix b₂ b₃ (toLin b₁ b₃ A) :=
by
cases nonempty_fintype κ
have := linearMap_toMatrix_mul_basis_toMatrix b₂ b₁ b₃ (Matrix.toLin b₁ b₃ A)
rwa [LinearMap.toMatrix_toLin] at this
