aeval_eq_aeval_mod_charpoly — Mathlib

English

See 130172: M^k = aeval M (X^k mod M.charpoly).

Русский

См. 130172: M^k = aeval M (X^k mod M.charpoly).

LaTeX

$$$$ M^{k} = \\operatorname{aeval}_{M}\\left( X^{k} \\bmod M^{\\text{charpoly}}\\right). $$$$

Lean4

/-- Any matrix polynomial `p` is equivalent under evaluation to `p %ₘ M.charpoly`; that is, `p`
is equivalent to a polynomial with degree less than the dimension of the matrix. -/
theorem aeval_eq_aeval_mod_charpoly (M : Matrix n n R) (p : R[X]) : aeval M p = aeval M (p %ₘ M.charpoly) :=
  (aeval_modByMonic_eq_self_of_root M.charpoly_monic M.aeval_self_charpoly).symm

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