charpoly_fromBlocks_zero₁₂ — Mathlib

English

If the top-right block is zero, the charpoly of fromBlocks equals the product of the charpolys of the diagonal blocks: χ_{fromBlocks M11 0 M21 M22} = χ_{M11} χ_{M22}.

Русский

Если верхнето-правый блок равен нулю, характеристический многочлен fromBlocks равен произведению характеристических многочленов диагональных блоков: χ_{fromBlocks M11 0 M21 M22} = χ_{M11} χ_{M22}.

LaTeX

$$$\operatorname{charpoly}\bigl(\operatorname{fromBlocks} M_{11} 0 M_{21} M_{22}\bigr) = \operatorname{charpoly}(M_{11}) \cdot \operatorname{charpoly}(M_{22})$$

Lean4

@[simp]
theorem charpoly_fromBlocks_zero₁₂ : (fromBlocks M₁₁ 0 M₂₁ M₂₂).charpoly = (M₁₁.charpoly * M₂₂.charpoly) := by
  simp only [charpoly, charmatrix_fromBlocks, Matrix.map_zero _ (Polynomial.C_0), neg_zero, det_fromBlocks_zero₁₂]

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