Commit 2022-06-23 14:10 966bb245

feat(group_theory/finite_abelian): Structure of finite abelian groups (#14736) Any finitely generated abelian group is the product of a power of ℤ and a direct sum of some zmod (p i ^ e i) for some prime powers p i ^ e i. Any finite abelian group is a direct sum of some zmod (p i ^ e i) for some prime powers p i ^ e i. (TODO : prove uniqueness of this decomposition)