coeff_charpolyRev_eq_neg_trace — Mathlib

English

The coefficient of X^1 in the reversed characteristic polynomial equals minus the trace of the matrix:

Русский

Коэффициент при X в степене 1 в обратном характеристическом многочлене равен минусу следа матрицы.

LaTeX

$$$\\bigl(\\mathrm{coeff}\\,\\mathrm{charpolyRev}\\,1\\bigr) = -\\mathrm{trace}(M)$$$

Lean4

@[simp]
theorem coeff_charpolyRev_eq_neg_trace (M : Matrix n n R) : coeff M.charpolyRev 1 = -trace M :=
  by
  nontriviality R
  cases isEmpty_or_nonempty n
  · simp [charpolyRev, coeff_one]
  · simp [trace_eq_neg_charpoly_coeff M, ← M.reverse_charpoly, nextCoeff]

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