hasEigenvalue_of_hasGenEigenvalue

English

All generalized eigenvalues are eigenvalues; equivalently, for any μ, k > 0, HasGenEigenvalue μ k implies HasEigenvalue μ.

Русский

Все обобщённые эйгензначения являются эйгензначениями; следовательно, для любого μ, k > 0, HasGenEigenvalue μ k следует HasEigenvalue μ.

LaTeX

$$$f.HasGenEigenvalue(μ,k) \\Rightarrow f.HasEigenvalue(μ) \\quad (k>0).$$$

Lean4

/-- All generalized eigenvalues are eigenvalues. -/
theorem hasEigenvalue_of_hasGenEigenvalue {f : End R M} {μ : R} {k : ℕ} (hμ : f.HasGenEigenvalue μ k) :
    f.HasEigenvalue μ :=
  hμ.lt zero_lt_one

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