Commit 2026-06-01 18:16 d31af3c3

View on Github →

feat(GroupTheory/Torsion): the free rank of an abelian group (#39972) This PR defines the rank of the free part of an abelian group.

Estimated changes

Modified Mathlib/GroupTheory/Rank.lean

Modified Mathlib/GroupTheory/Torsion.lean

added theorem CommGroup.freeRank_congr

added theorem CommGroup.freeRank_def

added theorem CommGroup.freeRank_eq_zero

added theorem CommGroup.freeRank_eq_zero_iff

added theorem CommGroup.freeRank_eq_zero_of_finite

added theorem CommGroup.freeRank_ge_of_surjective

added theorem CommGroup.le_comap_torsion

added theorem CommGroup.map_torsion_le