Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_comm_group.equiv_free_prod_direct_sum_zmod

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)
Modified add_comm_group.equiv_free_prod_direct_sum_zmodView on Github →
2022-06-23 14:10
src/group_theory/finite_abelian.lean
feat(group_theory/finite_abelian): Structure of finite abelian groups (#14736) …
Added add_comm_group.equiv_free_prod_direct_sum_zmodView on Github →