hasGenEigenvalue_iff — Mathlib

English

A generalized eigenvalue μ of rank k exists for f if and only if the generalized eigenspace is nontrivial, i.e., genEigenspace μ k ≠ ⊥.

Русский

Существование обобщённого эйгензначения μ для f ранга k эквивалентно не тривиальности соответствующего обобщённого эйгенпространства: genEigenspace μ k ≠ ⊥.

LaTeX

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

Lean4

theorem hasGenEigenvalue_iff {f : End R M} {μ : R} {k : ℕ} : f.HasGenEigenvalue μ k ↔ f.genEigenspace μ k ≠ ⊥ :=
  Iff.rfl

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