Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_comm_group.equiv_direct_sum_zmod_of_fintype

Modification history

2022-08-17 14:53
src/group_theory/finite_abelian.lean
chore(group_theory/*): Fix lint (#16095) …
Modified add_comm_group.equiv_direct_sum_zmod_of_fintypeView on Github →
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_direct_sum_zmod_of_fintypeView 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_direct_sum_zmod_of_fintypeView on Github →