charpoly_diagonal

Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

URI: https://scilib.ai/kg/mathlib#Matrix.charpoly_diagonal

English

If d: n → R, then the characteristic polynomial of diagonal(d) equals the product over i of (X − C(d(i))).

Русский

Если d: n → R, то χ_{diag(d)}(X) = ∏_{i} (X − C(d(i))).

LaTeX

$$$\operatorname{charpoly}(\operatorname{diagonal} d) = \prod_i (X - C(d(i)))$$$

Lean4

theorem charpoly_diagonal (d : n → R) : charpoly (diagonal d) = ∏ i, (X - C (d i)) := by simp [charpoly]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru