feat: Chinese Remainder Theorem for ZMod n (#29761)

Define `ZMod.equivPi`, the Chinese Remainder Theorem for `ZMod n`, decomposing it as a product of `ZMod` over its prime power factors.

Co-authored-by: bwangpj <70694994+bwangpj@users.noreply.github.com>

Author: bwangpj

Mathlib/Data/Nat/Factorization/Basic.lean

@@ -442,6 +442,20 @@ theorem prod_pow_prime_padicValNat (n : Nat) (hn : n ≠ 0) (m : Nat) (pr : n <
   · intro p hp
     simp [factorization_def n (prime_of_mem_primeFactors hp)]
 
+lemma prod_pow_primeFactors_factorization (hn : n ≠ 0) :
+    n = ∏ (p : n.primeFactors), (p : ℕ) ^ (n.factorization p) := by
+  nth_rw 1 [← factorization_prod_pow_eq_self hn]
+  rw [prod_factorization_eq_prod_primeFactors _]
+  exact prod_subtype n.primeFactors (fun _ ↦ Iff.rfl) fun a ↦ a ^ n.factorization a
+
+lemma pairwise_coprime_pow_primeFactors_factorization :
+    Pairwise (Function.onFun Nat.Coprime fun (p : n.primeFactors) ↦ p ^ n.factorization p) := by
+  intro p1 p2 hp
+  refine Nat.Coprime.pow (n.factorization p1) (n.factorization p2) ?_
+  refine (Nat.coprime_primes ?_ ?_).mpr <| Subtype.coe_ne_coe.mpr hp
+  · exact Nat.prime_of_mem_primeFactors p1.2
+  · exact Nat.prime_of_mem_primeFactors p2.2
+
 /-! ### Lemmas about factorizations of particular functions -/
 
 /-- Exactly `n / p` naturals in `[1, n]` are multiples of `p`.

Mathlib/Data/ZMod/QuotientRing.lean

@@ -6,6 +6,7 @@ Authors: Anne Baanen
 import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Int.Basic
 import Mathlib.RingTheory.ZMod
+import Mathlib.Data.Nat.Factorization.Basic
 
 /-!
 # `ZMod n` and quotient groups / rings
@@ -76,4 +77,11 @@ def ZMod.prodEquivPi {ι : Type*} [Fintype ι] (a : ι → ℕ)
   quotientInfRingEquivPiQuotient _ this |>.trans <|
   RingEquiv.piCongrRight fun i ↦ Int.quotientSpanNatEquivZMod (a i)
 
+/-- The **Chinese remainder theorem**, version for `ZMod n`. -/
+def ZMod.equivPi (hn : n ≠ 0) :
+    ZMod n ≃+* Π (p : n.primeFactors), ZMod (p ^ (n.factorization p)) :=
+  (ringEquivCongr <| Nat.prod_pow_primeFactors_factorization hn).trans
+    <| prodEquivPi (fun (p : n.primeFactors) ↦ (p : ℕ) ^ (n.factorization p))
+      n.pairwise_coprime_pow_primeFactors_factorization
+
 end ChineseRemainder