English
Under the Coprime on s hypothesis, the remainder of the list is strictly less than the product of the mapped s-values.
Русский
При гипотезе взаимной простоты на s остаток списка строго меньше произведения значений s на элементах списка.
LaTeX
$$$\mathrm{chineseRemainderOfList}\ a\ s\ l\ co < (l.map\, s).prod$$$
Lean4
theorem chineseRemainderOfList_lt_prod (l : List ι) (co : l.Pairwise (Coprime on s)) (hs : ∀ i ∈ l, s i ≠ 0) :
chineseRemainderOfList a s l co < (l.map s).prod := by
cases l with
| nil => simp
| cons i l =>
simp only [chineseRemainderOfList, List.map_cons, List.prod_cons]
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
refine chineseRemainder_lt_mul this (a i) (chineseRemainderOfList a s l co.of_cons) (hs i List.mem_cons_self) ?_
simp only [ne_eq, List.prod_eq_zero_iff, List.mem_map, not_exists, not_and]
intro j hj
exact hs j (List.mem_cons_of_mem _ hj)
