basis_toMatrix_mul_linearMap_toMatrix

English

A product formula: multiplying a basis matrix by a matrix A corresponds to the matrix of a composed linear map, up to a standard simplification.

Русский

Формула произведения: умножение матрицы базиса на матрицу A эквивалентно матрице композиции линейных отображений.

LaTeX

$$b1.toMatrix b2 * A = LinearMap.toMatrix b3 b1 (toLin b3 b2 A)$$

Lean4

@[simp]
theorem basis_toMatrix_mul_linearMap_toMatrix [Finite κ] [Fintype κ'] [DecidableEq ι'] :
    c.toMatrix c' * LinearMap.toMatrix b' c' f = LinearMap.toMatrix b' c f :=
  (Matrix.toLin b' c).injective <| by
    haveI := Classical.decEq κ'
    rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, LinearMap.id_comp]

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