torsion

Mathlib.GroupTheory.Torsion

URI: https://scilib.ai/kg/mathlib#CommGroup.torsion

Lean4

/-- The torsion subgroup of an abelian group. -/
@[to_additive /-- The torsion subgroup of an additive abelian group. -/
    ]
def torsion : Subgroup G :=
  { CommMonoid.torsion G with inv_mem' := fun hx => IsOfFinOrder.inv hx }

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

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

Разделы

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

Аффилиация

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