maxUnifEigenspaceIndex_le_finrank

English

For a finite-dimensional K-vector space V and f ∈ End_K(V), for any μ ∈ K, the maximal index of the generalized eigenspace is at most the dimension finrank_K V.

Русский

Для конечномерного пространства V над K и эндоморфизма f ∈ End_K(V) максимальный индекс общего пространства собственных значений по μ не превосходит размерности V.

LaTeX

$$$\maxUnifEigenspaceIndex f\, \mu \le \operatorname{finrank} K V$$$

Lean4

theorem maxUnifEigenspaceIndex_le_finrank [FiniteDimensional K V] (f : End K V) (μ : K) :
    maxUnifEigenspaceIndex f μ ≤ finrank K V := by
  apply Nat.sInf_le
  intro n hn
  apply le_antisymm
  · exact (f.genEigenspace μ).monotone <| WithTop.coeOrderHom.monotone hn
  · change (f.genEigenspace μ) n ≤ (f.genEigenspace μ) (finrank K V)
    rw [genEigenspace_nat, genEigenspace_nat]
    apply ker_pow_le_ker_pow_finrank

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