trace_eq_neg_charpoly_nextCoeff — Mathlib

English

The trace of M equals minus the coefficient of X^{card(n)−1} in the characteristic polynomial of M.

Русский

Сумма диагональных элементов (trace) матрицы M равна минусу коэффициента при X^{card(n)−1} в характеристическом полиномe M.

LaTeX

$$$$ \\operatorname{trace}(M) = - \\operatorname{charpoly}(M).coeff\\Big( |n| - 1 \\Big). $$$$

Lean4

theorem trace_eq_neg_charpoly_nextCoeff (M : Matrix n n R) : M.trace = -M.charpoly.nextCoeff :=
  by
  cases isEmpty_or_nonempty n
  · simp [nextCoeff]
  nontriviality
  simp [trace_eq_neg_charpoly_coeff, nextCoeff]

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