hasGenEigenvector_iff — Mathlib

English

A scalar μ is a generalized eigenvalue for a linear map f with exponent k if there exist generalized eigenvectors for f, μ, k.

Русский

Скаляр μ является обобщённым собственным значением для линейного отображения f с показателем k, если существуют обобщённые собственные векторы для f, μ, k.

LaTeX

$$$f \\text{ has generalized eigenvalue } \\mu \\text{ of order } k \\iff \\exists x \\neq 0,\\; x \\in \\mathrm{genEigenspace}(f, \\mu, k).$$$

Lean4

theorem hasGenEigenvector_iff {f : End R M} {μ : R} {k : ℕ} {x : M} :
    f.HasGenEigenvector μ k x ↔ x ∈ f.genEigenspace μ k ∧ x ≠ 0 :=
  Iff.rfl

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