charpoly_of_upperTriangular — Mathlib

English

If M is BlockTriangular with respect to the identity, then the characteristic polynomial factors as a product of diagonal block polynomials: χ_M = ∏ i∈image id univ χ_{M.toSquareBlock id i}.

Русский

Если M блок-верхнетреугольная по отношению к тождественному отображению, то χ_M раскладывается как произведение характеристических многочленов диагональных блоков: χ_M = ∏ χ_{M^{toSquareBlock}}.

LaTeX

$$$M.BlockTriangular\ id \Rightarrow M.charpoly = \prod a ∈ image id univ\; (M.toSquareBlock id a).charpoly$$

Lean4

theorem charpoly_of_upperTriangular [LinearOrder n] (M : Matrix n n R) (h : M.BlockTriangular id) :
    M.charpoly = ∏ i : n, (X - C (M i i)) := by
  simp [charpoly, det_of_upperTriangular h.charmatrix]
    -- This proof follows http://drorbn.net/AcademicPensieve/2015-12/CayleyHamilton.pdf

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