charpoly_sub_scalar — Mathlib

English

For any square matrix M and scalar μ, the characteristic polynomial of M − μ I equals the characteristic polynomial of M evaluated at X + μ, i.e., charpoly(M − μ I) = charpoly(M) ∘ (X + μ).

Русский

Для любой квадратной матрицы M и скаляра μ имеет место charpoly(M − μ I) = charpoly(M) под заменой X на X + μ.

LaTeX

$$$$ \\operatorname{charpoly}(M - \\mu I) = \\operatorname{charpoly}(M)\\big|_{X \\mapsto X + \\mu}. $$$$

Lean4

theorem charpoly_sub_scalar (M : Matrix n n R) (μ : R) : (M - scalar n μ).charpoly = M.charpoly.comp (X + C μ) :=
  by
  simp_rw [charpoly, det_apply, Polynomial.sum_comp, Polynomial.smul_comp, Polynomial.prod_comp]
  congr! with σ _ i _
  by_cases hi : σ i = i <;> simp [hi]
  ring

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