Commit 2023-07-05 18:37 f2c76a4c

View on Github →

feat: port GroupTheory.FiniteAbelian (#5730)

depends on: #4707

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/FiniteAbelian.lean

added theorem AddCommGroup.equiv_directSum_zMod_of_fintype

added theorem AddCommGroup.equiv_free_prod_directSum_zMod

added theorem AddCommGroup.finite_of_fG_torsion

added theorem CommGroup.finite_of_fG_torsion

added theorem Module.finite_of_fg_torsion