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.

Estimated changes