English
Multiplying a matrix M by the reindexed identity on the right yields the same as reindexing M accordingly.
Русский
Умножение M на переиндексированную единицу справа даёт тот же результат, что и переиндексация M соответствующим образом.
LaTeX
$$$ M \; \cdot \mathrm{reindexLinearEquiv}\ R\ A e_1 e_2 1 = \mathrm{reindexLinearEquiv}\ R\ A (\mathrm{id}_{m}) (e_1^{-1} \circ e_2)\, M. $$$
Lean4
theorem mul_reindexLinearEquiv_one [Fintype n] [DecidableEq o] (e₁ : o ≃ n) (e₂ : o ≃ n') (M : Matrix m n A) :
M * (reindexLinearEquiv R A e₁ e₂ 1) = reindexLinearEquiv R A (Equiv.refl m) (e₁.symm.trans e₂) M :=
haveI := Fintype.ofEquiv _ e₁.symm
mul_submatrix_one _ _ _