Theorem CharZero.of_isAddTorsionFree

Modification history

2026-01-13 19:40
Mathlib/Algebra/Module/Torsion/Free.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Added CharZero.of_isAddTorsionFreeView on Github →