basisFun_eq_pi_basisFun — Mathlib

English

A matrix identity expresses how a basis interacts with a linear map: multiplying the basis-by-A matrix by A yields a matrix whose i-th row is the coordinates of the image of the j-th basis vector under the basis repr.

Русский

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

LaTeX

$$$b.toMatrix (PiLp.basisFun p 𝕜 ι) \cdot A = Matrix.of (\lambda i j, b.repr (toLp(p, A^T j)) i)$$$

Lean4

theorem basisFun_eq_pi_basisFun : basisFun p 𝕜 ι = (Pi.basisFun 𝕜 ι).map (WithLp.linearEquiv p 𝕜 (ι → 𝕜)).symm :=
  rfl

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