instIsTriangularizableOfIsAlgClosed

English

If the base field K is algebraically closed and M is a finite-dimensional L-module, then the representation is triangularizable.

Русский

Если база — алгебраически закрытое поле K, и M — конечномерный модуль над Ли-алгеброй L, то представление треугольизируемо.

LaTeX

$$$[\text{IsAlgClosed }K] \Rightarrow \text{IsTriangularizable} \ K\ L\ M$$

Lean4

instance instIsTriangularizableOfIsAlgClosed [IsAlgClosed K] : IsTriangularizable K L M :=
  ⟨fun _ ↦ Module.End.iSup_maxGenEigenspace_eq_top _⟩

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