English
If a,b ∈ ℕ and l is a finite list of natural numbers with pairwise Coprime images under s, then a ≡ b (mod ∏ l_i) iff ∀ i ∈ l, a ≡ b (mod s i).
Русский
Пусть a,b ∈ ℕ и l — конечный список чисел such that значения s(i) для i ∈ l взаимно просты; тогда a ≡ b (mod ∏_{i∈l} s(i)) эквивалентно ∀ i ∈ l, a ≡ b (mod s(i)).
LaTeX
$$$a \equiv b \pmod{\prod_{i=0}^{|l|-1} l_i} \iff \forall i \in l, a \equiv b \pmod{l_i}$$$
Lean4
theorem modEq_list_prod_iff {a b} {l : List ℕ} (co : l.Pairwise Coprime) :
a ≡ b [MOD l.prod] ↔ ∀ i, a ≡ b [MOD l.get i] := by
induction l with
| nil => simp [modEq_one]
| cons m l ih =>
have : Coprime m l.prod := coprime_list_prod_right_iff.mpr (List.pairwise_cons.mp co).1
simp only [List.prod_cons, ← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co), List.length_cons]
constructor
· rintro ⟨h0, hs⟩ i
cases i using Fin.cases <;> simp_all
· intro h; exact ⟨h 0, fun i => h i.succ⟩
