Theorem CharZero.of_isAddTorsionFree

Modification history

2026-09-30 14:37

Mathlib/Algebra/Module/Torsion/Free.lean

refactor(Algebra/Group): fix the definition of torsion-free non-abelian groups (#42407) …

Deleted CharZero.of_isAddTorsionFree View on Github →

2026-01-13 19:40

Mathlib/Algebra/Module/Torsion/Free.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …

Added CharZero.of_isAddTorsionFree View on Github →