reindexLinearEquiv_comp_apply — Mathlib

English

The action of composing two reindexLinearEquiv maps on M equals applying the composed reindexLinearEquiv to M.

Русский

Действие композиции двух reindexLinearEquiv на матрице M совпадает с применением скомпозированной reindexLinearEquiv к M.

LaTeX

$$$ (\mathrm{reindexLinearEquiv}\ R\ A e_1' e_2') ( (\mathrm{reindexLinearEquiv}\ R\ A e_1 e_2) M) = \mathrm{reindexLinearEquiv}\ R\ A (e_1.trans e_1') (e_2.trans e_2') M. $$$

Lean4

theorem reindexLinearEquiv_comp_apply (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') (M : Matrix m n A) :
    (reindexLinearEquiv R A e₁' e₂') (reindexLinearEquiv R A e₁ e₂ M) =
      reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂') M :=
  submatrix_submatrix _ _ _ _ _

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