feat: Chinese remainder for ZMod. (#7599)

Mathlib/Data/ZMod/Quotient.lean

@@ -67,6 +67,22 @@ def quotientSpanEquivZMod (a : ℤ) : ℤ ⧸ Ideal.span ({a} : Set ℤ) ≃+* Z
 
 end Int
 
+noncomputable section ChineseRemainder
+open BigOperators Ideal
+
+/-- The **Chinese remainder theorem**, elementary version for `ZMod`. See also
+`Mathlib.Data.ZMod.Basic` for versions involving only two numbers. -/
+def ZMod.prodEquivPi {ι : Type*} [Fintype ι] (a : ι → ℕ)
+    (coprime : ∀ i j, i ≠ j → Nat.Coprime (a i) (a j)) : ZMod (∏ i, a i) ≃+* ∀ i, ZMod (a i) :=
+  have : ∀ (i j : ι), i ≠ j → IsCoprime (span {(a i : ℤ)}) (span {(a j : ℤ)}) :=
+    fun i j h ↦ (isCoprime_span_singleton_iff _ _).mpr ((coprime i j h).cast (R := ℤ))
+  Int.quotientSpanNatEquivZMod _ |>.symm.trans <|
+  quotEquivOfEq (iInf_span_singleton_natCast (R := ℤ) coprime) |>.symm.trans <|
+  quotientInfRingEquivPiQuotient _ this |>.trans <|
+  RingEquiv.piCongrRight fun i ↦ Int.quotientSpanNatEquivZMod (a i)
+
+end ChineseRemainder
+
 namespace AddAction
 
 open AddSubgroup AddMonoidHom AddEquiv Function

Mathlib/RingTheory/Coprime/Basic.lean

@@ -71,6 +71,13 @@ theorem not_isCoprime_zero_zero [Nontrivial R] : ¬IsCoprime (0 : R) 0 :=
   mt isCoprime_zero_right.mp not_isUnit_zero
 #align not_coprime_zero_zero not_isCoprime_zero_zero
 
+lemma IsCoprime.intCast {R : Type*} [CommRing R] {a b : ℤ} (h : IsCoprime a b) :
+    IsCoprime (a : R) (b : R) := by
+  rcases h with ⟨u, v, H⟩
+  use u, v
+  rw_mod_cast [H]
+  exact Int.cast_one
+
 /-- If a 2-vector `p` satisfies `IsCoprime (p 0) (p 1)`, then `p ≠ 0`. -/
 theorem IsCoprime.ne_zero [Nontrivial R] {p : Fin 2 → R} (h : IsCoprime (p 0) (p 1)) : p ≠ 0 := by
   rintro rfl

Mathlib/RingTheory/Coprime/Lemmas.lean

@@ -47,6 +47,12 @@ alias ⟨IsCoprime.nat_coprime, Nat.Coprime.isCoprime⟩ := Nat.isCoprime_iff_co
 #align is_coprime.nat_coprime IsCoprime.nat_coprime
 #align nat.coprime.is_coprime Nat.Coprime.isCoprime
 
+theorem Nat.Coprime.cast {R : Type*} [CommRing R] {a b : ℕ} (h : Nat.Coprime a b) :
+    IsCoprime (a : R) (b : R) := by
+  rw [← isCoprime_iff_coprime] at h
+  rw [← Int.cast_ofNat a, ← Int.cast_ofNat b]
+  exact IsCoprime.intCast h
+
 theorem ne_zero_or_ne_zero_of_nat_coprime {A : Type u} [CommRing A] [Nontrivial A] {a b : ℕ}
     (h : Nat.Coprime a b) : (a : A) ≠ 0 ∨ (b : A) ≠ 0 :=
   IsCoprime.ne_zero_or_ne_zero (R := A) <| by

Mathlib/RingTheory/Ideal/Operations.lean

@@ -632,13 +632,19 @@ theorem finset_inf_span_singleton {ι : Type*} (s : Finset ι) (I : ι → R)
   exact ⟨Finset.prod_dvd_of_coprime hI, fun h i hi => (Finset.dvd_prod_of_mem _ hi).trans h⟩
 #align ideal.finset_inf_span_singleton Ideal.finset_inf_span_singleton
 
-theorem iInf_span_singleton {ι : Type*} [Fintype ι] (I : ι → R)
+theorem iInf_span_singleton {ι : Type*} [Fintype ι] {I : ι → R}
     (hI : ∀ (i j) (_ : i ≠ j), IsCoprime (I i) (I j)) :
-    ⨅ i, Ideal.span ({I i} : Set R) = Ideal.span {∏ i, I i} := by
+    ⨅ i, span ({I i} : Set R) = span {∏ i, I i} := by
   rw [← Finset.inf_univ_eq_iInf, finset_inf_span_singleton]
   rwa [Finset.coe_univ, Set.pairwise_univ]
 #align ideal.infi_span_singleton Ideal.iInf_span_singleton
 
+theorem iInf_span_singleton_natCast {R : Type*} [CommRing R] {ι : Type*} [Fintype ι]
+    {I : ι → ℕ} (hI : ∀ (i j : ι), i ≠ j → (I i).Coprime (I j)) :
+    ⨅ (i : ι), span {(I i : R)} = span {((∏ i : ι, I i : ℕ) : R)} := by
+  rw [iInf_span_singleton, Nat.cast_prod]
+  exact fun i j h ↦ (hI i j h).cast
+
 theorem sup_eq_top_iff_isCoprime {R : Type*} [CommSemiring R] (x y : R) :
     span ({x} : Set R) ⊔ span {y} = ⊤ ↔ IsCoprime x y := by
   rw [eq_top_iff_one, Submodule.mem_sup]

Mathlib/RingTheory/Ideal/Quotient.lean

@@ -24,9 +24,6 @@ See `Algebra.RingQuot` for quotients of non-commutative rings.
 
  - `Ideal.Quotient`: the quotient of a commutative ring `R` by an ideal `I : Ideal R`
 
-## Main results
-
- - `Ideal.quotientInfRingEquivPiQuotient`: the **Chinese Remainder Theorem**
 -/
 
 

Mathlib/RingTheory/Ideal/QuotientOperations.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kenny Lau
+Authors: Kenny Lau, Patrick Massot
 -/
 import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.RingTheory.Ideal.Quotient
@@ -10,6 +10,13 @@ import Mathlib.RingTheory.Ideal.Quotient
 
 /-!
 # More operations on modules and ideals related to quotients
+
+## Main results:
+
+ - `quotientKerEquivRange` : the **first isomorphism theorem** for commutative rings.
+ - `Ideal.quotientInfRingEquivPiQuotient`: the **Chinese Remainder Theorem**, version for coprime
+   ideals (see also `ZMod.prodEquivPi` in `Data.ZMod.Quotient` for elementary versions about
+   `ZMod`).
 -/
 
 universe u v w