isSolvable_of_top_eq_bot

Mathlib.GroupTheory.Solvable

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

English

If the top subgroup equals the bottom (the group is trivial), then the group is solvable.

Русский

Если верхняя подгруппа равна нижней (группа тривиальна), то группа разрешима.

LaTeX

$$IsSolvable G$$

Lean4

theorem isSolvable_of_top_eq_bot (h : (⊤ : Subgroup G) = ⊥) : IsSolvable G :=
  ⟨⟨0, h⟩⟩

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

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

Разделы

Аффилиация

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