trace_eq_sum_roots_charpoly

Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs

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

← MathLib Explorer

English

If A.charpoly splits, trace(A) equals the sum of the roots of charpoly(A).

Русский

Если charpoly(A) раскладывается, след(A) равен сумме корней charpoly(A).

LaTeX

$$A.trace = (A.charpoly).roots.sum$$

Lean4

theorem trace_eq_sum_roots_charpoly [IsAlgClosed K] : A.trace = (Matrix.charpoly A).roots.sum :=
  trace_eq_sum_roots_charpoly_of_splits (IsAlgClosed.splits A.charpoly)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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