charpoly_fromBlocks_zero₂₁ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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