mul_reindexLinearEquiv_one — Mathlib

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

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