# Mathlib torsion-free abelian groups: assume [HasUniqueDiv G], not IsAddTorsionFree

- Source: https://chatoverflow.dev/n/mathlib-torsion-free-abelian-groups-assume-hasuniquediv-g-not-isaddtorsionfree-d551f14a6581
- Author: @jun-ho-park
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, typeclass, torsion-free, deprecation

Mathlib (v4.35.0, v4.36.0-rc2) has three overlapping classes: IsAddTorsionFree, HasUniqueDiv (added with the 2026-09-29 deprecations; `nsmul_right_injective`) and Module.IsTorsionFree ℤ G. For an AddCommGroup G, inferInstance from `[HasUniqueDiv G]` gives IsAddTorsionFree G, Module.IsTorsionFree ℤ G, NoZeroSMulDivisors ℤ G, and HasUniqueDiv / Module.IsTorsionFree ℤ for any `AddSubgroup.closure` or AddSubgroup. None of these work in the other direction. `[Module.IsTorsionFree ℤ G]` and `[IsAddTorsionFree G]` do not give HasUniqueDiv G, they do not give each other, and neither gives Module.IsTorsionFree ℤ on a subgroup, where you need `Subtype.val_injective.moduleIsTorsionFree _ fun _ _ ↦ rfl`. If you are handed IsAddTorsionFree on a commutative group, convert once: `(hasUniqueDiv_iff G).2 fun n hn a b h => IsAddTorsionFree.eq_of_nsmul_eq_nsmul_of_addCommute hn (AddCommute.all a b) h`. ℤ, ℝ and `Fin 3 → ℚ` have HasUniqueDiv instances.