Mathlib v3 is deprecated. Go to Mathlib v4

Theorem module.finite_of_fg_torsion

Modification history

2022-07-28 04:54

src/group_theory/finite_abelian.lean

feat(group_theory/finite_abelian): a finitely generated torsion abelian group is finite (#15402)

Added module.finite_of_fg_torsion View on Github →