charpoly — Mathlib

English

Equivalent version of the previous statement: the charmatrix of M.toSquareBlock b a equals M.charmatrix.toSquareBlock b a.

Русский

Эквивалентная версия: charmatrix(M.toSquareBlock b a) = charmatrix(M).toSquareBlock b a.

LaTeX

$$$\operatorname{charmatrix}\bigl( M.toSquareBlock\, b\, a \bigr) = \operatorname{charmatrix}(M)\,\text{toSquareBlock } b a$$$

Lean4

theorem charpoly {α : Type*} {b : n → α} [LinearOrder α] (h : M.BlockTriangular b) :
    M.charpoly = ∏ a ∈ image b univ, (M.toSquareBlock b a).charpoly := by
  simp only [Matrix.charpoly, h.charmatrix.det, charmatrix_toSquareBlock]

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