HasGenEigenvector — Mathlib

English

A nonzero element x of a generalized eigenspace is a generalized eigenvector of the operator with given eigenvalue and index.

Русский

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

LaTeX

$$$\\;x \\in \\mathrm{genEigenspace}(f, \\mu, k) \\wedge x \\neq 0 \\;\\Rightarrow\\; x \\text{ is a generalized eigenvector of } f \\text{ for } \\mu \\text{ of order } k.$$$

Lean4

/-- A nonzero element of a generalized eigenspace is a generalized eigenvector.
(Def 8.9 of [axler2015]) -/
abbrev HasGenEigenvector (f : End R M) (μ : R) (k : ℕ) (x : M) : Prop :=
  HasUnifEigenvector f μ k x

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