mathlib

7302e116 - feat(algebra/module/torsion): define torsion submodules (#12027)

feat(algebra/module/torsion): define torsion submodules (#12027) This file defines the a-torsion and torsion submodules for a R-module M and gives some basic properties. (The ultimate goal I'm working on is to classify the finitely-generated modules over a PID). Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>