reindex_apply — Mathlib

English

For any bijection e and Coxeter matrix M, the entry of the reindexed matrix equals the original entry at the preimage indices.

Русский

Для любой биекции e и матрицы Коксетера M элемент периндексированной матрицы равен соответствующему элементу исходной матрицы по предобразу индексов.

LaTeX

$$$$ (M.reindex\\ e\\ M)_{i i'} = M_{e^{-1}(i), e^{-1}(i')}. $$$$

Lean4

theorem reindex_apply (i i' : B') : M.reindex e i i' = M (e.symm i) (e.symm i') :=
  rfl

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