trace_eq_neg_charpoly_coeff — Mathlib

English

The same diagonal restriction bounds as in the diagonal degree lemma hold for the diagonal-subtracted characteristic polynomial.

Русский

Граница для диагонали сохраняется для подстановки диагонали в характеристический полином.

LaTeX

$$$$ \\deg\\Big( \\operatorname{charpoly}(M) - \\prod_{i} (X - C(M_{ii})) \\Big) < |n| - 1. $$$$

Lean4

/-- See also `Matrix.coeff_charpolyRev_eq_neg_trace`. -/
theorem trace_eq_neg_charpoly_coeff [Nonempty n] (M : Matrix n n R) :
    trace M = -M.charpoly.coeff (Fintype.card n - 1) :=
  by
  rw [charpoly_coeff_eq_prod_coeff_of_le _ le_rfl, Fintype.card,
    prod_X_sub_C_coeff_card_pred univ (fun i : n => M i i) Fintype.card_pos, neg_neg, trace]
  simp_rw [diag_apply]

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