finite_hasEigenvalue — Mathlib

English

There are finitely many eigenvalues of a linear endomorphism on a finite-dimensional space.

Русский

Для линейного отображения на конечномерном пространстве конечное число собственных значений.

LaTeX

$$$$ \#\{\mu \mid f \text{ has eigenvalue } \mu\} < \infty. $$$$

Lean4

theorem finite_hasEigenvalue : Set.Finite f.HasEigenvalue :=
  by
  have h : minpoly R f ≠ 0 := minpoly.ne_zero (Algebra.IsIntegral.isIntegral (R := R) f)
  convert (minpoly R f).rootSet_finite R
  ext μ
  change f.HasEigenvalue μ ↔ _
  rw [hasEigenvalue_iff_isRoot, mem_rootSet_of_ne h, IsRoot, coe_aeval_eq_eval]

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