English
Let e be a bijection between index sets m and n, and M a square matrix of size m with entries in A. Then relabelling the rows and columns of M by e using the AlgEquiv construction yields the matrix obtained by the standard index relabelling; i.e., reindexAlgEquiv R A e M = reindex e e M.
Русский
Пусть e — биекция между множествами индексов m и n, а M — квадратная матрица размерности m над кольцом A. Тогда перенос индексов по e как по обеим осям с помощью преобразования AlgEquiv совпадает с обычной реиндексацией матрицы: reindexAlgEquiv R A e M = reindex e e M.
LaTeX
$$$ (\mathrm{reindexAlgEquiv}\ R\ A\ e)\, M = (\mathrm{reindex}\ e\ e)\, M $$$
Lean4
@[simp]
theorem reindexAlgEquiv_apply (e : m ≃ n) (M : Matrix m m A) : reindexAlgEquiv R A e M = reindex e e M :=
rfl
