Theorem isTorsionFree_iff_noZeroSMulDivisors_nat

Modification history

2024-10-08 17:07
Mathlib/GroupTheory/Torsion.lean
feat: `IsTorsionFree ↔ NoZeroSMulDivisors` aliases (#17307) …
Deleted isTorsionFree_iff_noZeroSMulDivisors_natView on Github →
2024-02-29 21:30
Mathlib/GroupTheory/Torsion.lean
feat: `IsTorsionFree M ↔ NoZeroSMulDivisors ℕ M` (#10918) …
Added isTorsionFree_iff_noZeroSMulDivisors_natView on Github →