eval_charpoly — Mathlib

English

For every t in the base ring, the evaluation of the characteristic polynomial at t equals the determinant of tI − M.

Русский

Для любого t в основании кольца значение χ_M(t) равно детерминанту от tI − M.

LaTeX

$$$\operatorname{charpoly}(M)(t) = \det(tI - M)$$$

Lean4

theorem eval_charpoly (M : Matrix m m R) (t : R) : M.charpoly.eval t = (Matrix.scalar _ t - M).det :=
  by
  rw [Matrix.charpoly, ← Polynomial.coe_evalRingHom, RingHom.map_det, Matrix.charmatrix]
  congr
  ext i j
  obtain rfl | hij := eq_or_ne i j <;> simp [*]

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