mathlib

6c7b880e - feat(algebra/module/torsion): torsion ideal, decomposition lemma (#13414)

feat(algebra/module/torsion): torsion ideal, decomposition lemma (#13414) Defines the torsion ideal of an element in a module, and also shows a decomposition lemma for torsion modules. Co-authored-by: pbazin <75327486+pbazin@users.noreply.github.com>