reindex_refl_refl — Mathlib

English

Reindexing with identity equivalences leaves the matrix unchanged: reindex (Equiv.refl _) (Equiv.refl _) A = A.

Русский

Реиндексация на единичных эквивалентностях оставляет матрицу без изменений: reindex (Equiv.refl _) (Equiv.refl _) A = A.

LaTeX

$$$\text{reindex}(\mathrm{Equiv.refl\, _},\mathrm{Equiv.refl\, _})\ A = A$$$

Lean4

theorem reindex_refl_refl (A : Matrix m n α) : reindex (Equiv.refl _) (Equiv.refl _) A = A :=
  A.submatrix_id_id

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