isTorsion_of_finite

Mathlib.GroupTheory.Torsion

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

← MathLib Explorer

English

Finite groups are torsion groups.

Русский

Конечные группы являются торсионными.

LaTeX

$$$[Finite\ G]\Rightarrow IsTorsion(G)$$$

Lean4

/-- Finite groups are torsion groups. -/
@[to_additive is_add_torsion_of_finite /-- Finite additive groups are additive torsion groups. -/
    ]
theorem isTorsion_of_finite [Finite G] : IsTorsion G :=
  ExponentExists.isTorsion .of_finite

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

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

Разделы

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

Аффилиация

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