finrank_maxGenEigenspace_eq — Mathlib

English

The finite rank of the zero generalized eigenspace equals the root multiplicity of the eigenvalue in the charpoly.

Русский

Конечная размерность нулевого обобщённого эйгенпространства равна кратности корня эйгензначения в характеристической полиномии.

LaTeX

$$finrank K (φ.maxGenEigenspace μ) = φ.charpoly.rootMultiplicity μ$$

Lean4

theorem finrank_maxGenEigenspace_eq (φ : Module.End K M) (μ : K) :
    finrank K (φ.maxGenEigenspace μ) = φ.charpoly.rootMultiplicity μ := by
  rw [φ.maxGenEigenspace_eq_maxGenEigenspace_zero, finrank_maxGenEigenspace_zero_eq,
    Polynomial.rootMultiplicity_eq_natTrailingDegree, LinearMap.charpoly_sub_smul]

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