English
A vector x is a uniform eigenvector of f with eigenvalue μ and index k if x lies in the μ-generalized eigenspace of index k and x ≠ 0.
Русский
Вектор x является обобщённым собственным вектором f с собственным значением μ и индексом k, если x принадлежит μ-обобщённому собственному пространству индекса k и x ≠ 0.
LaTeX
$$HasUnifEigenvector(f, μ, k, x) := x ∈ f.genEigenspace(μ, k) ∧ x ≠ 0$$
Lean4
/-- Let `M` be an `R`-module, and `f` an `R`-linear endomorphism of `M`,
and let `μ : R` and `k : ℕ∞` be given.
Then `x : M` satisfies `HasUnifEigenvector f μ k x` if
`x ∈ f.genEigenspace μ k` and `x ≠ 0`.
For `k = 1`, this means that `x` is an eigenvector of `f` with eigenvalue `μ`. -/
def HasUnifEigenvector (f : End R M) (μ : R) (k : ℕ∞) (x : M) : Prop :=
x ∈ f.genEigenspace μ k ∧ x ≠ 0
