instFiniteSpectrum

Mathlib.LinearAlgebra.Eigenspace.Minpoly

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

English

Reiterates that the spectrum of a matrix is finite as an instance.

Русский

Повторно утверждается, что спектр матрицы конечен.

LaTeX

$$$$ \operatorname{Finite}(\operatorname{spectrum}(R,A)). $$$$

Lean4

instance instFiniteSpectrum (A : Matrix n n R) : Finite (spectrum R A) :=
  Set.finite_coe_iff.mpr (Matrix.finite_spectrum A)

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

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

Разделы

Аффилиация

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