instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd

English

If M is triangularizable under the action of L, then the range of the corresponding endomorphism representation on M is triangularizable.

Русский

Если M треугольна по действию L, то диапазон представления эндоморфизмов на M треугольизируем.

LaTeX

$$$\text{IsTriangularizable}(R,L,M) \Rightarrow \text{IsTriangularizable}(R,(\mathrm{LieModule}.toEnd\,R\,L\,M).\mathrm{range},M)$$$

Lean4

instance [IsTriangularizable R L M] : IsTriangularizable R (LieModule.toEnd R L M).range M where
  maxGenEigenspace_eq_top := by
    rintro ⟨-, x, rfl⟩
    exact IsTriangularizable.maxGenEigenspace_eq_top x

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