solvable_quotient_of_solvable

Mathlib.GroupTheory.Solvable

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

← MathLib Explorer

English

If H ⫽ G is normal and G is solvable, then G/H is solvable.

Русский

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

LaTeX

$$IsSolvable (G ⧸ H)$$

Lean4

instance solvable_quotient_of_solvable (H : Subgroup G) [H.Normal] [IsSolvable G] : IsSolvable (G ⧸ H) :=
  solvable_of_surjective (QuotientGroup.mk'_surjective H)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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