English
Reindexing respects matrix multiplication: for e : m ≃ n and M, N ∈ Matrix m m A, we have reindexAlgEquiv R A e (M * N) = (reindexAlgEquiv R A e M) * (reindexAlgEquiv R A e N).
Русский
Реиндексация сохраняет произведение матриц: для e : m ≃ n и матриц M, N ∈ Matrix m m A выполняется reindexAlgEquiv R A e (M * N) = (reindexAlgEquiv R A e M) · (reindexAlgEquiv R A e N).
LaTeX
$$$ \mathrm{reindexAlgEquiv}\ R\ A\ e (M N) = (\mathrm{reindexAlgEquiv}\ R\ A\ e) M \cdot (\mathrm{reindexAlgEquiv}\ R\ A\ e) N $$$
Lean4
theorem reindexAlgEquiv_mul (e : m ≃ n) (M : Matrix m m A) (N : Matrix m m A) :
reindexAlgEquiv R A e (M * N) = reindexAlgEquiv R A e M * reindexAlgEquiv R A e N :=
map_mul ..