eval_charpoly — Mathlib

English

The Cayley–Hamilton theorem holds: applying the characteristic polynomial of f to f yields zero; i.e., aeval f f.charpoly = 0.

Русский

Теорема о Кайли–Гамильтоне: при применении характеристического многочлена к f получается ноль; aeval f f.charpoly = 0.

LaTeX

$$aeval\ f\ f.charpoly = 0$$

Lean4

theorem eval_charpoly (t : R) : f.charpoly.eval t = (algebraMap _ _ t - f).det := by
  rw [charpoly, Matrix.eval_charpoly, ← LinearMap.det_toMatrix (chooseBasis R M), map_sub, scalar_apply,
    toMatrix_algebraMap, scalar_apply]

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