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