charpoly_reindex — Mathlib

English

Another formulation: the characteristic polynomial after reindexing by e equals the original characteristic polynomial, i.e., χ_{reindex e e M} = χ_M.

Русский

Ещё одно формулирование: характеристический многочлен после переиндексации по e равен исходному, χ_{reindex e e M} = χ_M.

LaTeX

$$$\operatorname{charpoly}(\operatorname{reindex} e e M) = \operatorname{charpoly}(M)$$$

Lean4

theorem charpoly_reindex (e : n ≃ m) (M : Matrix n n R) : (reindex e e M).charpoly = M.charpoly :=
  by
  unfold Matrix.charpoly
  rw [charmatrix_reindex, Matrix.det_reindex_self]

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