reindexLinearEquiv_mul — Mathlib

English

Reindexing respects matrix multiplication: reindexed M times reindexed N equals the reindexed product MN.

Русский

Переиндексация сохраняет умножение матриц: переиндексированное M умножить на переиндексированное N равно переиндексированному MN.

LaTeX

$$$ \mathrm{reindexLinearEquiv}\ R\ A e_m e_n M \; \cdot \; \mathrm{reindexLinearEquiv}\ R\ A e_n e_o N = \mathrm{reindexLinearEquiv}\ R\ A e_m e_o (M N). $$$

Lean4

theorem reindexLinearEquiv_mul [Fintype n] [Fintype n'] (eₘ : m ≃ m') (eₙ : n ≃ n') (eₒ : o ≃ o') (M : Matrix m n A)
    (N : Matrix n o A) :
    reindexLinearEquiv R A eₘ eₙ M * reindexLinearEquiv R A eₙ eₒ N = reindexLinearEquiv R A eₘ eₒ (M * N) :=
  submatrix_mul_equiv M N _ _ _

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