reindexAlgEquiv_mul — Mathlib

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 ..

Похожие утверждения