Theorem CommGroup.freeRank_eq_zero_of_finite

Modification history

2026-06-01 18:16
Mathlib/GroupTheory/Torsion.lean
feat(GroupTheory/Torsion): the free rank of an abelian group (#39972) …
Added CommGroup.freeRank_eq_zero_of_finiteView on Github →