charmatrix_reindex — Mathlib

English

Reindexing a matrix by a bijection preserves its charmatrix up to the same reindexing: charmatrix(reindex e e M) = reindex e e (charmatrix M).

Русский

Перебиндирование матрицы по биекциям сохраняет характеристическую матрицу, примененную к ней: charmatrix(reindex e e M) = reindex e e (charmatrix M).

LaTeX

$$$\operatorname{charmatrix}\bigl(\operatorname{reindex} \, e \, e \, M\bigr) = \operatorname{reindex} \, e \, e \, (\operatorname{charmatrix}(M))$$$

Lean4

theorem charmatrix_reindex (e : n ≃ m) : charmatrix (reindex e e M) = reindex e e (charmatrix M) :=
  by
  ext i j x
  by_cases h : i = j
  all_goals simp [h]

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