basis_toMatrix_mul — Mathlib

English

A generalizes the previous product formula to arbitrary bases and matrices: b1.toMatrix b2 * A equals the matrix of the composed map.

Русский

Обобщение на произвольные базисы: произведение матриц базиса и A равно матрице композиции линейного отображения.

LaTeX

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

Lean4

theorem basis_toMatrix_mul [Fintype κ] [Finite ι] [DecidableEq κ] (b₁ : Basis ι R M) (b₂ : Basis ι' R M)
    (b₃ : Basis κ R N) (A : Matrix ι' κ R) : b₁.toMatrix b₂ * A = LinearMap.toMatrix b₃ b₁ (toLin b₃ b₂ A) :=
  by
  have := basis_toMatrix_mul_linearMap_toMatrix b₃ b₁ b₂ (Matrix.toLin b₃ b₂ A)
  rwa [LinearMap.toMatrix_toLin] at this

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