theorem AbelianGroups.fundamental_theorem_finite_abelian_groups (G : Type u_1) [AddCommGroup G] [Finite G] : ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ), Nonempty (G ≃+ DirectSum ι fun (i : ι) => ZMod (p i ^ e i))

theorem AbelianGroups.elementary_divisors_to_invariant_factors (ι : Type u_1) [Fintype ι] (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ) : ∃ (k : ℕ) (d : Fin k → ℕ), (∀ (i : Fin k), 1 < d i) ∧ (∀ (i j : Fin k), i ≤ j → d i ∣ d j) ∧ Nonempty ((DirectSum ι fun (i : ι) => ZMod (p i ^ e i)) ≃+ DirectSum (Fin k) fun (i : Fin k) => ZMod (d i))

theorem AbelianGroups.fundamental_theorem_fg_abelian_groups_invariant_factors (A : Type u_1) [AddCommGroup A] [AddGroup.FG A] : ∃ (a : ℕ) (k : ℕ) (d : Fin k → ℕ), (∀ (i : Fin k), 1 < d i) ∧ (∀ (i j : Fin k), i ≤ j → d i ∣ d j) ∧ Nonempty (A ≃+ (Fin a →₀ ℤ) × DirectSum (Fin k) fun (i : Fin k) => ZMod (d i))

theorem AbelianGroups.torsion_subgroup_structure (A : Type u_1) [AddCommGroup A] [AddGroup.FG A] : ∃ (n : ℕ) (d : Fin n → ℕ) (_ : ∀ (i : Fin n), 0 < d i), Nonempty (↥(AddCommGroup.torsion A) ≃+ DirectSum (Fin n) fun (i : Fin n) => ZMod (d i))