English
Reindexing composes: (reindex e_m e_n).trans (reindex e_m2 e_n2) = reindex (e_m.trans e_m2) (e_n.trans e_n2).
Русский
Реиндексация по композиции: (reindex e_m e_n).trans (reindex e_m2 e_n2) = reindex (e_m.trans e_m2) (e_n.trans e_n2).
LaTeX
$$$ (\mathrm{reindex}\ e_m\ e_n).trans (\mathrm{reindex}\ e_{m2}\ e_{n2}) = \mathrm{reindex} (e_m.\mathrm{trans} e_{m2}) (e_n.\mathrm{trans} e_{n2}) $$$
Lean4
@[simp]
theorem reindex_trans {l₂ o₂ : Type*} (eₘ : m ≃ l) (eₙ : n ≃ o) (eₘ₂ : l ≃ l₂) (eₙ₂ : o ≃ o₂) :
(reindex eₘ eₙ).trans (reindex eₘ₂ eₙ₂) = (reindex (eₘ.trans eₘ₂) (eₙ.trans eₙ₂) : Matrix m n α ≃ _) :=
Equiv.ext fun A => (A.submatrix_submatrix eₘ.symm eₙ.symm eₘ₂.symm eₙ₂.symm :)
