Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_comm_group.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 add_comm_group.finite_of_fg_torsionView on Github →