maxGenEigenspace_eq_genEigenspace_finrank

English

In a finite-dimensional setting, the maximal generalized eigenspace equals the generalized eigenspace at the finite rank equal to the dimension (finrank V).

Русский

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

LaTeX

$$$f.maxGenEigenspace(\\mu) = f.genEigenspace(\\mu, \\mathrm{finrank}(K,V)).$$$

Lean4

theorem maxGenEigenspace_eq_genEigenspace_finrank [FiniteDimensional K V] (f : End K V) (μ : K) :
    f.maxGenEigenspace μ = f.genEigenspace μ (finrank K V) :=
  by
  apply le_antisymm _ <| (f.genEigenspace μ).monotone le_top
  rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]
  apply genEigenspace_le_genEigenspace_finrank f μ

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