mul_toMatrix_toPEquiv — Mathlib

English

For a finite m and bijection σ: m ≃ n, the vecMul after mapping equals the function composition with σ^{-1}.

Русский

Для конечного множества m и биекции σ: m ≃ n vecMul после отображения равен композиции функции с σ^{-1}.

LaTeX

$$$\\sigma.toPEquiv.toMatrix \\; \\text{mulVec} \\; a = a \\circ \\sigma^{-1}$$$

Lean4

theorem mul_toMatrix_toPEquiv [Fintype m] [DecidableEq n] [NonAssocSemiring α] (M : Matrix l m α) (f : m ≃ n) :
    (M * f.toPEquiv.toMatrix) = M.submatrix id f.symm :=
  Matrix.ext fun i j => by
    rw [PEquiv.mul_toMatrix_apply, ← Equiv.toPEquiv_symm, Equiv.toPEquiv_apply, Matrix.submatrix_apply, id]

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