HasGenEigenvalue — Mathlib

English

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

Русский

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

LaTeX

$$$f.HasGenEigenvalue\\;\\mu\\;k \\text{ iff } \\exists x \\neq 0, x \\in \\mathrm{genEigenspace}(f, \\mu, k).$$$

Lean4

/-- A scalar `μ` is a generalized eigenvalue for a linear map `f` and an exponent `k ∈ ℕ` if there
are generalized eigenvectors for `f`, `k`, and `μ`. -/
abbrev HasGenEigenvalue (f : End R M) (μ : R) (k : ℕ) : Prop :=
  HasUnifEigenvalue f μ k

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