Torsion-free modules?

Stream: Is there code for X?

[Jz Pan]

Seems that we don't have torsion-free modules Module.IsTorsionFree, but we can always use Submodule.torsion R M = ⊥. We also don't have properties of torsion-free modules, e.g. a finitely generated torsion-free module over a Dedekind domain is projective.

[Yaël Dillies]

A month ago I PRed #22962, which is torsion-free ℕ-modules. My hope was to PR torsion-free modules after that one had landed

[Yaël Dillies]

Torsion-free ℕ-modules are important to have separately because we want the multiplicative version too, that uses ℕ powers

[Andrew Yang]

For modules over domains you could just use NoZeroSMulDivisors or FaithfulSMul. But I agree we probably want a Module.IsTorsionFree.