exists_eigenvalue — Mathlib

English

Over an algebraically closed field K, every finite-dimensional endomorphism f of a nontrivial vector space V has an eigenvalue.

Русский

Над алгебраически замкнутым полем K любой конечномерный линейный оператор f на негомомологичном пространстве V имеет собственное значение.

LaTeX

$$$\\exists c \\in K, f.HasEigenvalue(c)$$$

Lean4

/-- In finite dimensions, over an algebraically closed field, every linear endomorphism has an
eigenvalue. -/
theorem exists_eigenvalue [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f : End K V) :
    ∃ c : K, f.HasEigenvalue c := by
  simp_rw [hasEigenvalue_iff_mem_spectrum]
  exact spectrum.nonempty_of_isAlgClosed_of_finiteDimensional K f

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