Commit 2022-06-13 19:21 a75460f3

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).

• depends on: #13414
• depends on: #14376
• depends on: #14573