Theorem CommGroup.finite_of_fg_torsion

Modification history

2026-07-24 18:27

Mathlib/GroupTheory/FiniteAbelian/Basic.lean

chore(GroupTheory/Torsion): rename `IsTorsion` to `IsMulTorsion` (#41213) …

Deleted CommGroup.finite_of_fg_torsion View on Github →

2023-07-18 03:34

Mathlib/GroupTheory/FiniteAbelian.lean

chore: tidy various files (#5971)

Added CommGroup.finite_of_fg_torsion View on Github →