instFiniteElemRealSpectrum

Mathlib.LinearAlgebra.Matrix.Spectrum

URI: https://scilib.ai/kg/mathlib#Matrix.instFiniteElemRealSpectrum

English

The spectrum over the real numbers of a finite-dimensional matrix is finite (as a set of real eigenvalues).

Русский

Спектр над множеством действительных чисел конечен (как множество действительных собственных значений).

LaTeX

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

Lean4

instance [DecidableEq n] : Finite (spectrum ℝ A) :=
  A.finite_real_spectrum

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru