finrank_eigenspace_le — Mathlib

English

The geometric multiplicity (dimension of eigenspace) of μ is at most the algebraic multiplicity given by the rootMultiplicity.

Русский

Геометрическая кратность эйгензначения μ не превосходит алгебраическую кратность, задаваемую rootMultiplicity.

LaTeX

$$finrank K (φ.eigenspace μ) ≤ φ.charpoly.rootMultiplicity μ$$

Lean4

/-- The geometric multiplicity of an eigenvalue is at most the algebraic multiplicity. -/
theorem finrank_eigenspace_le (φ : Module.End K M) (μ : K) :
    finrank K (φ.eigenspace μ) ≤ φ.charpoly.rootMultiplicity μ :=
  finrank_genEigenspace_le ..

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