Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-28 04:54 adeda57b

View on Github →

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

Estimated changes

Modified src/group_theory/finite_abelian.lean

modified theorem add_comm_group.equiv_direct_sum_zmod_of_fintype

modified theorem add_comm_group.equiv_free_prod_direct_sum_zmod

added theorem add_comm_group.finite_of_fg_torsion

added theorem comm_group.finite_of_fg_torsion

added theorem module.finite_of_fg_torsion