charpoly_sub_smul — Mathlib

English

For a linear endomorphism f and a scalar μ, the characteristic polynomial of f − μ·1 equals the polynomial of f evaluated at X+Cμ.

Русский

Для отображения f и скаляра μ характеристический многочлен f − μ·1 равен характеристическому многочлену f, подставляющему X+Cμ.

LaTeX

$$f.charpoly_sub_smul μ = (f.charpoly).comp (X + C μ)$$

Lean4

theorem charpoly_sub_smul (f : Module.End R M) (μ : R) : (f - μ • 1).charpoly = f.charpoly.comp (X + C μ) := by
  simpa [LinearMap.charpoly, smul_eq_mul_diagonal] using Matrix.charpoly_sub_scalar ..

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