mathlib

966bb245 - feat(group_theory/finite_abelian): Structure of finite abelian groups (#14736)

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)