English
If z is congruent to each a(i) modulo s(i) for i ∈ l, then z is congruent to the Chinese remainder of the list modulo the product.
Русский
Если z ≡ a(i) (mod s(i)) для всех i ∈ l, то z ≡ ChineseRemainderOfList(a,s,l) (mod prod).
LaTeX
$$$(\forall i ∈ l, z \equiv a_i \pmod{s_i}) \Rightarrow z \equiv \mathrm{chineseRemainderOfList}\ a\ s\ l\ co \pmod{(l.map\, s).prod}$$$
Lean4
theorem chineseRemainderOfList_modEq_unique (l : List ι) (co : l.Pairwise (Coprime on s)) {z}
(hz : ∀ i ∈ l, z ≡ a i [MOD s i]) : z ≡ chineseRemainderOfList a s l co [MOD (l.map s).prod] := by
induction l with
| nil => simp [modEq_one]
| cons i l ih =>
simp only [List.map_cons, List.prod_cons, chineseRemainderOfList]
have : Coprime (s i) (l.map s).prod :=
by
simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
intro j hj
exact (List.pairwise_cons.mp co).1 j hj
exact
chineseRemainder_modEq_unique this (hz i List.mem_cons_self)
(ih co.of_cons (fun j hj => hz j (List.mem_cons_of_mem _ hj)))
