English
Evaluating any polynomial p at f is equivalent to evaluating p modulo its characteristic polynomial at f.
Русский
Для любого полинома p при подстановке в f эквивалентно вычисление p по модулю от характерполинома f.
LaTeX
$$aeval f p = aeval f (p %ₘ f.charpoly)$$
Lean4
/-- The **Cayley-Hamilton Theorem**, that the characteristic polynomial of a linear map, applied
to the linear map itself, is zero.
See `Matrix.aeval_self_charpoly` for the equivalent statement about matrices. -/
theorem aeval_self_charpoly : aeval f f.charpoly = 0 :=
by
apply (LinearEquiv.map_eq_zero_iff (algEquivMatrix (chooseBasis R M)).toLinearEquiv).1
rw [AlgEquiv.toLinearEquiv_apply, ← AlgEquiv.coe_algHom, ← Polynomial.aeval_algHom_apply _ _ _, charpoly_def]
exact Matrix.aeval_self_charpoly _
