linearMap_toMatrix_mul_basis_toMatrix

English

For bases b, b', c, c' and a linear map f, the matrix of f with respect to bases b',c' times the basis-change matrix equals the matrix of f with respect to bases b,c'.

Русский

Для баз b, b', c, c' и линейного отображения f матрица f относительно баз b',c' умноженная на соответствующую матрицу перехода даёт матрицу f относительно баз b,c'.

LaTeX

$$$\\mathrm{toMatrix}_{b',c'}(f) \\cdot \\mathrm{toMatrix}_{b'}(b) = \\mathrm{toMatrix}_{b,c'}(f)$$$

Lean4

@[simp]
theorem linearMap_toMatrix_mul_basis_toMatrix [Finite κ'] [DecidableEq ι] [DecidableEq ι'] :
    LinearMap.toMatrix b' c' f * b'.toMatrix b = LinearMap.toMatrix b c' f :=
  (Matrix.toLin b c').injective <| by
    rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, LinearMap.comp_id]

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