isSolvable_of_subsingleton

Mathlib.GroupTheory.Solvable

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

← MathLib Explorer

English

A subsingleton group is solvable.

Русский

Группа с единственным элементом является разрешимой.

LaTeX

$$IsSolvable G$$

Lean4

instance (priority := 100) isSolvable_of_subsingleton [Subsingleton G] : IsSolvable G :=
  isSolvable_of_top_eq_bot G (by simp [eq_iff_true_of_subsingleton])

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

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

Разделы

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

Аффилиация

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