isSolvable_of_comm

Mathlib.GroupTheory.Solvable

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

← MathLib Explorer

English

If a group is abelian (commutative), then it is solvable.

Русский

Если группа коммутативна, то она разрешима.

LaTeX

$$IsSolvable G$$

Lean4

theorem isSolvable_of_comm {G : Type*} [hG : Group G] (h : ∀ a b : G, a * b = b * a) : IsSolvable G :=
  by
  letI hG' : CommGroup G := { hG with mul_comm := h }
  cases hG
  exact CommGroup.isSolvable

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

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

Разделы

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

Аффилиация

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