Commit 2026-01-20 08:34 044bc75f
View on Github →chore(Algebra): replace NoZeroSMulDivisors with Module.IsTorsionFree, losing generality (#33873)
NoZeroSMulDivisors R M is mathematically wrong when R isn't a domain, so we replace it with the better definition Module.IsTorsionFree R M whenever they are equivalent.
This PR continues #30563, replacing NoZeroSMulDivisors R M with Module.IsTorsionFree R M even when this loses generality.