toMatrix_trans — Mathlib

English

The transitive mapping of PEquiv compositions correlates with matrix multiplication.

Русский

Транзитивное отображение композиции PEquiv связано с умножением матриц.

LaTeX

$$$((f.trans g).toMatrix) = f.toMatrix · g.toMatrix$$$

Lean4

theorem toMatrix_trans [Fintype m] [DecidableEq m] [DecidableEq n] [NonAssocSemiring α] (f : l ≃. m) (g : m ≃. n) :
    ((f.trans g).toMatrix : Matrix l n α) = f.toMatrix * g.toMatrix :=
  by
  ext i j
  rw [toMatrix_mul_apply]
  dsimp [toMatrix, PEquiv.trans]
  cases f i <;> simp

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