instFintypeEigenvalues — Mathlib

English

If a family of endomorphisms is pairwise commuting and each is triangularizable, then they are simultaneously triangularizable.

Русский

Если семейство взаимно коммутирует и каждое треугольно, то они треугольны одновременно.

LaTeX

$$$$ \bigvee_{\chi:\iota\to K} \bigwedge_{i} \maxGenEigenspace((f_i),(\chi(i))) = \top. $$$$

Lean4

/-- An endomorphism of a finite-dimensional vector space has finitely many eigenvalues. -/
noncomputable instance : Fintype f.Eigenvalues :=
  Set.Finite.fintype f.finite_hasEigenvalue

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