pow_eq_aeval_mod_charpoly — Mathlib

English

For a square matrix M over a commutative ring, every power M^k equals aeval M (X^k mod charpoly(M)).

Русский

Для квадратной матрицы M над коммутативным кольцом каждый показатель M^k равен aeval(M, X^k mod charpoly(M)).

LaTeX

$$$ M^k = aeval\_M (X^k \\bmod \\mathrm{charpoly}(M)) $$$

Lean4

/-- Any matrix power can be computed as the sum of matrix powers less than `Fintype.card n`.

TODO: add the statement for negative powers phrased with `zpow`. -/
theorem pow_eq_aeval_mod_charpoly (M : Matrix n n R) (k : ℕ) : M ^ k = aeval M (X ^ k %ₘ M.charpoly) := by
  rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]

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