Theorem noZeroSMulDivisors_nat_iff_isAddTorsionFree

Modification history

2026-01-20 08:34
Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree`, losing generality (#33873) …
Deleted noZeroSMulDivisors_nat_iff_isAddTorsionFreeView on Github →
2025-05-14 07:47
Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean
feat: more lemmas about torsion-free monoids (#24312) …
Added noZeroSMulDivisors_nat_iff_isAddTorsionFreeView on Github →