English
If a finite family of elements is pairwise coprime, the radical of their product equals the product of their radicals.
Русский
Если конечная семья элементов попарно взаимно проста, то радикал их произведения равен произведению радикалов элементов.
LaTeX
$$$\operatorname{radical}\left( \prod_{i\in s} f(i) \right) = \prod_{i\in s} \operatorname{radical}(f(i))$$$
Lean4
theorem radical_prod {ι : Type*} {f : ι → M} (s : Finset ι)
(h : Set.Pairwise (s : Set ι) (Function.onFun IsRelPrime f)) : radical (∏ i ∈ s, f i) = ∏ i ∈ s, radical (f i) := by
induction s using Finset.cons_induction with
| empty => simp
| cons i s his ih =>
simp only [Finset.prod_cons]
rw [Finset.coe_cons, Set.pairwise_insert_of_symmetric_of_notMem (symmetric_isRelPrime.comap _) (by simpa)] at h
rw [radical_mul, ih h.1]
exact IsRelPrime.prod_right h.2
