reindex_apply — Mathlib

English

The reindex map applied to a matrix equals the corresponding submatrix with inverse index maps: reindex e_m e_n M = M.submatrix e_m^{-1} e_n^{-1}.

Русский

Применение реиндексации к матрице эквивалентно подматрице с обратными отображениями индексов: reindex e_m e_n M = M.submatrix e_m^{-1} e_n^{-1}.

LaTeX

$$$ \mathrm{reindex}\ e_m\ e_n\ M = M.submatrix\ e_m^{-1}\ e_n^{-1} $$$

Lean4

@[simp]
theorem reindex_apply (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) : reindex eₘ eₙ M = M.submatrix eₘ.symm eₙ.symm :=
  rfl

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