instIsTriangularizableSubtypeMemLieSubalgebra

English

If M is triangularizable under the action of a Lie algebra L, then M remains triangularizable when the action is restricted to any Lie subalgebra L' of L.

Русский

Если M треугольна по действию над L, то при ограничении действия на подалгебру L' ⊆ L треугольность сохраняется.

LaTeX

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

Lean4

instance (L' : LieSubalgebra R L) [IsTriangularizable R L M] : IsTriangularizable R L' M where
  maxGenEigenspace_eq_top x := IsTriangularizable.maxGenEigenspace_eq_top (x : L)

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