pow_eq_aeval_mod_charpoly — Mathlib

English

For any polynomial p, evaluating p at f is equal to evaluating the remainder of p modulo f.charpoly at f.

Русский

Для любого полинома p вычисление p(f) равно вычислению остатка p mod f.charpoly на f.

LaTeX

$$aeval f p = aeval f (p %ₘ f.charpoly)$$

Lean4

/-- Any endomorphism power can be computed as the sum of endomorphism powers less than the
dimension of the module. -/
theorem pow_eq_aeval_mod_charpoly (k : ℕ) : f ^ k = aeval f (X ^ k %ₘ f.charpoly) := by
  rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]

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