finrank_genEigenspace_le — Mathlib

English

For any μ, the dimension of the genEigenspace μ k is bounded above by the root multiplicity of μ in the charpoly of φ.

Русский

Для любого μ размерность genEigenspace μ k не превышает кратность μ в charpoly φ.

LaTeX

$$finrank K (φ.genEigenspace μ k) ≤ φ.charpoly.rootMultiplicity μ$$

Lean4

theorem finrank_genEigenspace_le (φ : Module.End K M) (μ : K) (k : ℕ) :
    finrank K (φ.genEigenspace μ k) ≤ φ.charpoly.rootMultiplicity μ := by
  grw [Submodule.finrank_mono (φ.genEigenspace_le_maximal μ k), finrank_maxGenEigenspace_eq]

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