English
There exists a residue k modulo ∏ i∈l s(i) such that k ≡ a(i) (mod s(i)) for all i ∈ l, provided the s(i) are nonzero and pairwise coprime on s.
Русский
Существует остаток k modulo ∏_{i∈l} s(i) такой, что k ≡ a(i) (mod s(i)) для всех i ∈ l, при условии s(i) ≠ 0 и взаимной простоты.
LaTeX
$$$\exists! k \in \mathbb{N}\;\forall i \in l,\; k \equiv a_i \pmod{s_i} \wedge k < (l.map\, s).prod$$$
Lean4
/-- The natural number less than `(l.map s).prod` congruent to
`a i` mod `s i` for all `i ∈ l`. -/
def chineseRemainderOfList : (l : List ι) → l.Pairwise (Coprime on s) → { k // ∀ i ∈ l, k ≡ a i [MOD s i] }
| [], _ => ⟨0, by simp⟩
| i :: l, co =>
by
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
have ih := chineseRemainderOfList l co.of_cons
have k := chineseRemainder this (a i) ih
use k
simp only [List.mem_cons, forall_eq_or_imp, k.prop.1, true_and]
intro j hj
exact ((modEq_list_map_prod_iff co.of_cons).mp k.prop.2 j hj).trans (ih.prop j hj)
