subgroup_solvable_of_solvable

Mathlib.GroupTheory.Solvable

URI: https://scilib.ai/kg/mathlib#subgroup_solvable_of_solvable

English

If H ≤ G and G is solvable, then H is solvable.

Русский

Если H подгруппа G и G разрешима, то и H разрешима.

LaTeX

$$IsSolvable H$$

Lean4

instance subgroup_solvable_of_solvable (H : Subgroup G) [IsSolvable G] : IsSolvable H :=
  solvable_of_solvable_injective H.subtype_injective

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

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

Разделы

Аффилиация

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