Theorem Module.isTorsionFree_iff_smul_eq_zero

Modification history

2026-01-26 15:41

Mathlib/Algebra/Module/Torsion/Free.lean

chore(Algebra): deprecate a few more `NoZeroSMulDivisors` lemmas (#34203) …

Modified Module.isTorsionFree_iff_smul_eq_zero View on Github →

2026-01-12 13:34

Mathlib/Algebra/Module/Torsion/Free.lean

feat(Algebra): more `Module.IsTorsionFree` API (#33871) …

Added Module.isTorsionFree_iff_smul_eq_zero View on Github →