instIsTriangularizableSubtypeMemLieSubmodule

English

If M is triangularizable as a module over a Lie algebra L, then it is triangularizable as a module over any Lie ideal I of L.

Русский

Если M треугольна как модуль над L, то она треугольна и как модуль над любом идеальной подалгеброй I ⊆ L.

LaTeX

$$$\text{IsTriangularizable}(R,L,M) \Rightarrow \text{IsTriangularizable}(R,I,M)$$$

Lean4

instance (I : LieIdeal R L) [IsTriangularizable R L M] : IsTriangularizable R I M where
  maxGenEigenspace_eq_top x := IsTriangularizable.maxGenEigenspace_eq_top (x : L)

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