instIsSolvableSubtypeMemLieSubmodule

Mathlib.Algebra.Lie.Solvable

URI: https://scilib.ai/kg/mathlib#Function.instIsSolvableSubtypeMemLieSubmodule

English

If I is a solvable Lie ideal of L, then any Lie-submodule/subtype determined by I is solvable.

Русский

Если I — разрешимый Ли-идеал L, то любая подструктура на основе I разрешима.

LaTeX

$$$\text{IsSolvable } I \Rightarrow \text{IsSolvable } (\text{Subtype } x \in I)$$$

Lean4

instance (A : LieIdeal R L) [IsSolvable L] : IsSolvable A :=
  A.incl_injective.lieAlgebra_isSolvable

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

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

Разделы

Аффилиация

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