instIsSolvableSubtypeMemLieSubalgebraTop

Mathlib.Algebra.Lie.Solvable

URI: https://scilib.ai/kg/mathlib#LieAlgebra.instIsSolvableSubtypeMemLieSubalgebraTop

English

If L is solvable, then the top Lie subalgebra (i.e., L itself) is solvable.

Русский

Если L разрешима, то верхняя подпогруппа Ли-алгебра L разрешима.

LaTeX

$$$[IsSolvable L] \Rightarrow [IsSolvable (\top : \text{LieSubalgebra } R L)]$$$

Lean4

instance [IsSolvable L] : IsSolvable (⊤ : LieSubalgebra R L) := by
  rwa [solvable_iff_equiv_solvable LieSubalgebra.topEquiv]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru