Commit 2025-11-06 12:18 26a4b33d

feat(Algebra/Module/Torsion): more instances (#30716) Split Algebra.Module.Torsion into Algebra.Module.Torsion.Free for torsion-free modules and Algebra.Module.Torsion.Basic for torsion modules. Add prod and pi instances, as well as pullback instances and the fact that a torsion-free module over a char zero domain is a torsion-free group.