English
Let a,b ∈ ℕ, s : ι → ℕ, l : List ι with L.Pairwise Coprime on s. Then a ≡ b (mod (l.map s).prod) iff ∀ i ∈ l, a ≡ b (mod s i).
Русский
Пусть a,b ∈ ℕ, s : ι → ℕ, l : List ι с попарно взаимно простыми значениями s; тогда a ≡ b (mod (List.map s l).prod) ⇔ ∀ i ∈ l, a ≡ b (mod s i).
LaTeX
$$$a \equiv b \pmod{(\mathrm{List.map}\, s\, l).prod} \iff \forall i \in l, a \equiv b \pmod{s(i)}$$$
Lean4
theorem modEq_list_map_prod_iff {a b} {s : ι → ℕ} {l : List ι} (co : l.Pairwise (Coprime on s)) :
a ≡ b [MOD (l.map s).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i] := by
induction l with
| nil => simp [modEq_one]
| cons i l
ih =>
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
simp [← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co)]
