English
The Chinese Remainder Theorem for ZMod: for a finite index set ι and a_i ∈ ℕ with pairwise coprime on a, there is a ring isomorphism ZMod(∏ a_i) ≅ ∏ ZMod(a_i).
Русский
Китайская теорема об остатках для ZMod: существует кольцевое изоморфление ZMod(∏ a_i) ≅ ∏ ZMod(a_i), когда множества a_i попарно разборчивы.
LaTeX
$$$$ \\mathrm{ZMod}\\left(\\prod_{i} a_i\\right) \\cong \\prod_{i} \\mathrm{ZMod}(a_i). $$$$
Lean4
/-- The **Chinese remainder theorem**, elementary version for `ZMod`. See also
`Mathlib/Data/ZMod/Basic.lean` for versions involving only two numbers. -/
def prodEquivPi {ι : Type*} [Fintype ι] (a : ι → ℕ) (coprime : Pairwise (Nat.Coprime on a)) :
ZMod (∏ i, a i) ≃+* Π i, ZMod (a i) :=
have : Pairwise fun i j => IsCoprime (span {(a i : ℤ)}) (span {(a j : ℤ)}) := fun _i _j h ↦
(isCoprime_span_singleton_iff _ _).mpr ((coprime 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)
