mathlib3

a75460f3 - feat(algebra/module/pid): Classification of finitely generated torsion modules over a PID (#13524)

feat(algebra/module/pid): Classification of finitely generated torsion modules over a PID (#13524) A finitely generated torsion module over a PID is isomorphic to a direct sum of some `R ⧸ R ∙ (p i ^ e i)` where the `p i ^ e i` are prime powers. (TODO : This part should be generalisable to a Dedekind domain, see https://en.wikipedia.org/wiki/Dedekind_domain#Finitely_generated_modules_over_a_Dedekind_domain . Part of the proof is already generalised). More generally, a finitely generated module over a PID is isomorphic to the product of a free module and a direct sum of some `R ⧸ R ∙ (p i ^ e i)`. (TODO : prove this decomposition is unique.) (TODO : deduce the structure theorem for finite(ly generated) abelian groups). - [x] depends on: #13414 - [x] depends on: #14376 - [x] depends on: #14573 Co-authored-by: pbazin <75327486+pbazin@users.noreply.github.com>