finite_spectrum — Mathlib

English

An ending matrix has a finite spectrum as an instance statement.

Русский

Конечномерная матрица имеет конечный спектр как инстанс.

LaTeX

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

Lean4

/-- An n x n matrix over a field has a finite spectrum. -/
theorem finite_spectrum (A : Matrix n n R) : Set.Finite (spectrum R A) :=
  by
  rw [← AlgEquiv.spectrum_eq (Matrix.toLinAlgEquiv <| Pi.basisFun R n) A]
  exact Module.End.finite_spectrum _

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