English
Finite abelian group is a direct sum of cyclic p-power groups ZMod(p^e).
Русский
Конечная абелева группа является прямой суммой циклических групп-помен: ZMod(p^e).
LaTeX
$$$G \cong_+ \bigoplus_{i \in ι} \mathbb{Z}/p_i^{e_i}\mathbb{Z}$$$
Lean4
/-- **Structure theorem of finitely generated abelian groups** : 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`. -/
theorem equiv_free_prod_directSum_zmod [hG : AddGroup.FG G] :
∃ (n : ℕ) (ι : Type) (_ : Fintype ι) (p : ι → ℕ) (_ : ∀ i, Nat.Prime <| p i) (e : ι → ℕ),
Nonempty <| G ≃+ (Fin n →₀ ℤ) × ⨁ i : ι, ZMod (p i ^ e i) :=
by
obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ :=
@Module.equiv_free_prod_directSum _ _ _ _ _ _ _ (Module.Finite.iff_addGroup_fg.mpr hG)
refine ⟨n, ι, fι, fun i => (p i).natAbs, fun i => ?_, e, ⟨?_⟩⟩
· rw [← Int.prime_iff_natAbs_prime, ← irreducible_iff_prime]; exact hp i
exact
f.toAddEquiv.trans
((AddEquiv.refl _).prodCongr <|
DFinsupp.mapRange.addEquiv fun i =>
((Int.quotientSpanEquivZMod _).trans <| ZMod.ringEquivCongr <| (p i).natAbs_pow _).toAddEquiv)
