reindexLinearEquiv_one — Mathlib

English

Reindexing a 1×1 identity matrix by the same index is still the identity.

Русский

Переиндексация единичной квадратной матрицы тем же индексом сохраняет тождественность.

LaTeX

$$$ \mathrm{reindexLinearEquiv}\ R\ A e\, e\; (1_{m\times m}) = 1_{m\times m}. $$$

Lean4

theorem reindexLinearEquiv_one [DecidableEq m] [DecidableEq m'] [One A] (e : m ≃ m') :
    reindexLinearEquiv R A e e (1 : Matrix m m A) = 1 :=
  submatrix_one_equiv e.symm

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