reindexLinearEquiv_apply — Mathlib

English

The map reindexLinearEquiv R A e_m e_n M equals the matrix obtained by reindexing M by e_m and e_n.

Русский

Отображение reindexLinearEquiv R A e_m e_n M совпадает с матрицей, полученной переиндексацией M по e_m и e_n.

LaTeX

$$$ (\mathrm{reindexLinearEquiv}\ R\ A\ e_m\ e_n\ M) = (\mathrm{reindex}\ e_m\ e_n\ M). $$$

Lean4

@[simp]
theorem reindexLinearEquiv_apply (eₘ : m ≃ m') (eₙ : n ≃ n') (M : Matrix m n A) :
    reindexLinearEquiv R A eₘ eₙ M = reindex eₘ eₙ M :=
  rfl

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