finite_real_spectrum — Mathlib

English

The real spectrum of a square matrix is finite; i.e., a matrix has only finitely many real eigenvalues.

Русский

Спектр действительных значений квадратной матрицы конечен, то есть у матрицы конечное число действительных собственных значений.

LaTeX

$$$\#\operatorname{spectrum}_{\mathbb{R}}(A) < \infty$$$

Lean4

theorem finite_real_spectrum [DecidableEq n] : (spectrum ℝ A).Finite :=
  by
  rw [← spectrum.preimage_algebraMap 𝕜]
  exact A.finite_spectrum.preimage (FaithfulSMul.algebraMap_injective ℝ 𝕜).injOn

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