English
If pairwise IsCoprime on s holds and each s_i divides z, then product ∏ s_i divides z.
Русский
Если пары IsCoprime на s выполняется и каждый s_i делит z, тогда произведение делит z.
LaTeX
$$$(t.toSet).Pairwise (Function.onFun IsCoprime s) \Rightarrow (\forall i, i∈t → s_i \mid z) \Rightarrow (\prod i\in t, s_i) \mid z$$$
Lean4
theorem prod_dvd_of_coprime (Hs : (t : Set I).Pairwise (IsCoprime on s)) (Hs1 : (∀ i ∈ t, s i ∣ z)) :
(∏ x ∈ t, s x) ∣ z := by
classical
induction t using Finset.induction_on with
| empty => simp
| insert a r har ih =>
rw [Finset.prod_insert har]
refine IsCoprime.mul_dvd ?_ ?_ ?_
· refine IsCoprime.prod_right fun i hir ↦ ?_
exact Hs (by simp) (by simp [hir]) (ne_of_mem_of_not_mem hir har).symm
· exact Hs1 a (Finset.mem_insert_self a r)
· refine ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi
simp only [Finset.coe_insert, Set.subset_insert]
