English
If a family {s(i)} is pairwise coprime relative to x and every s(i) divides z, then the product ∏_{i∈t} s(i) divides z.
Русский
Если пара единиц {s(i)} взаимно проста относительно x и каждый s(i) делится на z, то произведение делится на z.
LaTeX
$$(t : Set I).Pairwise (IsRelPrime on s) → (∀ i ∈ t, s i ∣ z) → (∏ x ∈ t, s x) ∣ z$$
Lean4
theorem prod_dvd_of_isRelPrime : (t : Set I).Pairwise (IsRelPrime on s) → (∀ i ∈ t, s i ∣ z) → (∏ x ∈ t, s x) ∣ z := by
classical
exact
Finset.induction_on t (fun _ _ ↦ one_dvd z)
(by
intro a r har ih Hs Hs1
rw [Finset.prod_insert har]
have aux1 : a ∈ (↑(insert a r) : Set I) := Finset.mem_insert_self a r
refine
(IsRelPrime.prod_right fun i hir ↦
Hs aux1 (Finset.mem_insert_of_mem hir) <| by
rintro rfl
exact har hir).mul_dvd
(Hs1 a aux1) (ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi)
simp only [Finset.coe_insert, Set.subset_insert])
