feat: Variant of structure theorem of finite abelian groups (#10587)

where the trivial factors have been dropped.

I have the idea of a general approach to dropping trivial terms from a direct sum. However it is too complicated for me to unsorry it and overkill here, so I am leaving it as a comment.

From LeanAPAP

Mathlib/Data/ZMod/Basic.lean

@@ -854,6 +854,18 @@ def chineseRemainder {m n : ℕ} (h : m.Coprime n) : ZMod (m * n) ≃+* ZMod m 
     right_inv := inv.2 }
 #align zmod.chinese_remainder ZMod.chineseRemainder
 
+lemma subsingleton_iff {n : ℕ} : Subsingleton (ZMod n) ↔ n = 1 := by
+  constructor
+  · obtain (_ | _ | n) := n
+    · simpa [ZMod] using not_subsingleton _
+    · simp [ZMod]
+    · simpa [ZMod] using not_subsingleton _
+  · rintro rfl
+    infer_instance
+
+lemma nontrivial_iff {n : ℕ} : Nontrivial (ZMod n) ↔ n ≠ 1 := by
+  rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]
+
 -- todo: this can be made a `Unique` instance.
 instance subsingleton_units : Subsingleton (ZMod 2)ˣ :=
   ⟨by decide⟩

Mathlib/GroupTheory/FiniteAbelian.lean

@@ -14,14 +14,74 @@ import Mathlib.Data.ZMod.Quotient
 * `AddCommGroup.equiv_free_prod_directSum_zmod` : 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`.
-* `AddCommGroup.equiv_directSum_zmod_of_fintype` : Any finite abelian group is a direct sum of
+* `AddCommGroup.equiv_directSum_zmod_of_finite` : Any finite abelian group is a direct sum of
   some `ZMod (p i ^ e i)` for some prime powers `p i ^ e i`.
 
 -/
 
-
 open scoped DirectSum
 
+/-
+TODO: Here's a more general approach to dropping trivial factors from a direct sum:
+
+def DirectSum.congr {ι κ : Type*} {α : ι → Type*} {β : κ → Type*} [DecidableEq ι] [DecidableEq κ]
+    [∀ i, DecidableEq (α i)] [∀ j, DecidableEq (β j)] [∀ i, AddCommMonoid (α i)]
+    [∀ j, AddCommMonoid (β j)] (f : ∀ i, Nontrivial (α i) → κ) (g : ∀ j, Nontrivial (β j) → ι)
+    (F : ∀ i hi, α i →+ β (f i hi)) (G : ∀ j hj, β j →+ α (g j hj))
+    (hfg : ∀ i hi hj, g (f i hi) hj = i) (hgf : ∀ j hj hi, f (g j hj) hi = j)
+    (hFG : ∀ i hi hj a, hfg i hi hj ▸ G _ hj (F i hi a) = a)
+    (hGF : ∀ j hj hi b, hgf j hj hi ▸ F _ hi (G j hj b) = b) :
+    (⨁ i, α i) ≃+ ⨁ j, β j where
+  toFun x := x.sum fun i a ↦ if ha : a = 0 then 0 else DFinsupp.single (f i ⟨a, 0, ha⟩) (F _ _ a)
+  invFun y := y.sum fun j b ↦ if hb : b = 0 then 0 else DFinsupp.single (g j ⟨b, 0, hb⟩) (G _ _ b)
+  -- The two sorries here are probably doable with the existing machinery, but quite painful
+  left_inv x := DFinsupp.ext fun i ↦ sorry
+  right_inv y := DFinsupp.ext fun j ↦ sorry
+  map_add' x₁ x₂ := by
+    dsimp
+    refine DFinsupp.sum_add_index (by simp) fun i a₁ a₂ ↦ ?_
+    split_ifs
+    any_goals simp_all
+    rw [← DFinsupp.single_add, ← map_add, ‹a₁ + a₂ = 0›, map_zero, DFinsupp.single_zero]
+
+private def directSumNeZeroMulEquiv (ι : Type) [DecidableEq ι] (p : ι → ℕ) (n : ι → ℕ) :
+    (⨁ i : {i // n i ≠ 0}, ZMod (p i ^ n i)) ≃+ ⨁ i, ZMod (p i ^ n i) :=
+  DirectSum.congr
+    (fun i _ ↦ i)
+    (fun j hj ↦ ⟨j, fun h ↦ by simp [h, pow_zero, zmod_nontrivial] at hj⟩)
+    (fun i _ ↦ AddMonoidHom.id _)
+    (fun j _ ↦ AddMonoidHom.id _)
+    (fun i hi hj ↦ rfl)
+    (fun j hj hi ↦ rfl)
+    (fun i hi hj a ↦ rfl)
+    (fun j hj hi a ↦ rfl)
+-/
+
+private def directSumNeZeroMulHom {ι : Type} [DecidableEq ι] (p : ι → ℕ) (n : ι → ℕ) :
+    (⨁ i : {i // n i ≠ 0}, ZMod (p i ^ n i)) →+ ⨁ i, ZMod (p i ^ n i) :=
+  DirectSum.toAddMonoid fun i ↦ DirectSum.of (fun i ↦ ZMod (p i ^ n i)) i
+
+private def directSumNeZeroMulEquiv (ι : Type) [DecidableEq ι] (p : ι → ℕ) (n : ι → ℕ) :
+    (⨁ i : {i // n i ≠ 0}, ZMod (p i ^ n i)) ≃+ ⨁ i, ZMod (p i ^ n i) where
+  toFun := directSumNeZeroMulHom p n
+  invFun := DirectSum.toAddMonoid fun i ↦
+    if h : n i = 0 then 0 else DirectSum.of (fun j : {i // n i ≠ 0} ↦ ZMod (p j ^ n j)) ⟨i, h⟩
+  left_inv x := by
+    induction' x using DirectSum.induction_on with i x x y hx hy
+    · simp
+    · rw [directSumNeZeroMulHom, DirectSum.toAddMonoid_of, DirectSum.toAddMonoid_of,
+        dif_neg i.prop]
+    · rw [map_add, map_add, hx, hy]
+  right_inv x := by
+    induction' x using DirectSum.induction_on with i x x y hx hy
+    · rw [map_zero, map_zero]
+    · rw [DirectSum.toAddMonoid_of]
+      split_ifs with h
+      · simp [(ZMod.subsingleton_iff.2 $ by rw [h, pow_zero]).elim x 0]
+      · simp_rw [directSumNeZeroMulHom, DirectSum.toAddMonoid_of]
+    · rw [map_add, map_add, hx, hy]
+  map_add' := map_add (directSumNeZeroMulHom p n)
+
 universe u
 
 namespace Module
@@ -68,7 +128,7 @@ theorem equiv_free_prod_directSum_zmod [hG : AddGroup.FG G] :
 
 /-- **Structure theorem of finite abelian groups** : Any finite abelian group is a direct sum of
 some `ZMod (p i ^ e i)` for some prime powers `p i ^ e i`. -/
-theorem equiv_directSum_zmod_of_fintype [Finite G] :
+theorem equiv_directSum_zmod_of_finite [Finite G] :
     ∃ (ι : Type) (_ : Fintype ι) (p : ι → ℕ) (_ : ∀ i, Nat.Prime <| p i) (e : ι → ℕ),
       Nonempty <| G ≃+ ⨁ i : ι, ZMod (p i ^ e i) := by
   cases nonempty_fintype G
@@ -81,7 +141,20 @@ theorem equiv_directSum_zmod_of_fintype [Finite G] :
     exact
       (Fintype.ofSurjective (fun f : Fin n.succ →₀ ℤ => f 0) fun a =>
             ⟨Finsupp.single 0 a, Finsupp.single_eq_same⟩).false.elim
-#align add_comm_group.equiv_direct_sum_zmod_of_fintype AddCommGroup.equiv_directSum_zmod_of_fintype
+#align add_comm_group.equiv_direct_sum_zmod_of_fintype AddCommGroup.equiv_directSum_zmod_of_finite
+
+/-- **Structure theorem of finite abelian groups** : Any finite abelian group is a direct sum of
+some `ZMod (q i)` for some prime powers `q i > 1`. -/
+lemma equiv_directSum_zmod_of_finite' (G : Type*) [AddCommGroup G] [Finite G] :
+    ∃ (ι : Type) (_ : Fintype ι) (n : ι → ℕ),
+      (∀ i, 1 < n i) ∧ Nonempty (G ≃+ ⨁ i, ZMod (n i)) := by
+  classical
+  obtain ⟨ι, hι, p, hp, n, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite G
+  skip
+  refine ⟨{i : ι // n i ≠ 0}, inferInstance, fun i ↦ p i ^ n i, ?_,
+    ⟨e.trans (directSumNeZeroMulEquiv ι _ _).symm⟩⟩
+  rintro ⟨i, hi⟩
+  exact one_lt_pow (hp _).one_lt hi
 
 theorem finite_of_fg_torsion [hG' : AddGroup.FG G] (hG : AddMonoid.IsTorsion G) : Finite G :=
   @Module.finite_of_fg_torsion _ _ _ (Module.Finite.iff_addGroup_fg.mpr hG') <|