finite_spectrum — Mathlib

English

An n×n matrix over a field has a finite spectrum.

Русский

Матрица n×n над полем имеет конечный спектр.

LaTeX

$$$$ \#\operatorname{spectrum}(R,A) < \infty. $$$$

Lean4

/-- An endomorphism of a finite-dimensional vector space has a finite spectrum. -/
theorem finite_spectrum {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V]
    (f : Module.End K V) : Set.Finite (spectrum K f) :=
  by
  convert f.finite_hasEigenvalue
  ext f x
  exact Module.End.hasEigenvalue_iff_mem_spectrum.symm

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