hasEigenvalue_iff_mem_spectrum — Mathlib

English

In finite dimensions, HasEigenvalue μ is equivalent to μ being in the spectrum.

Русский

В конечномерном случае HasEigenvalue μ эквивалентно μ принадлежит спектру.

LaTeX

$$HasEigenvalue(f, μ) ⇔ μ ∈ spectrum(f) (finite-dimensional case)$$

Lean4

theorem hasEigenvalue_iff_mem_spectrum [FiniteDimensional K V] {f : End K V} {μ : K} :
    f.HasEigenvalue μ ↔ μ ∈ spectrum K f :=
  hasUnifEigenvalue_iff_mem_spectrum

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