English
Reindexing a matrix along equivariant type indexes produces a natural equivalence between matrices with different index sets.
Русский
Реиндексация матрицы по эквиваленциям типов порождает естественное эквивалентное отображение между матрицами с различными индексами.
LaTeX
$$$\text{reindex }(e_m,e_n) : \mathrm{Matrix}\,m n\alpha \simeq \mathrm{Matrix}\,l o\alpha $$$
Lean4
/-- The natural map that reindexes a matrix's rows and columns with equivalent types is an
equivalence. -/
def reindex (eₘ : m ≃ l) (eₙ : n ≃ o) : Matrix m n α ≃ Matrix l o α
where
toFun M := M.submatrix eₘ.symm eₙ.symm
invFun M := M.submatrix eₘ eₙ
left_inv M := by simp
right_inv M := by simp
