English
If a finite set of elements is pairwise coprime and each is squarefree, then their product is squarefree.
Русский
Если конечное множество элементов попарно взаимно просто и каждый элемент квадратно свободен, то их произведение квадратно свободно.
LaTeX
$$$\forall i, \mathrm{Squarefree}(f(i)) \land \text{PairwiseIsRelPrime}(f) \Rightarrow \mathrm{Squarefree}\bigl(\prod_{i\in s} f(i)\bigr)$$$
Lean4
theorem squarefree_prod_of_pairwise_isCoprime {ι : Type*} {s : Finset ι} {f : ι → R}
(hs : Set.Pairwise s.toSet (IsRelPrime on f)) (hs' : ∀ i ∈ s, Squarefree (f i)) : Squarefree (∏ i ∈ s, f i) := by
induction s using Finset.cons_induction with
| empty => simp
| cons a s ha ih =>
rw [Finset.prod_cons, squarefree_mul_iff]
rw [Finset.coe_cons, Set.pairwise_insert] at hs
refine ⟨.prod_right fun i hi ↦ ?_, hs' a (by simp), ?_⟩
· exact (hs.right i (by simp [hi]) fun h ↦ ha (h ▸ hi)).left
· exact ih hs.left fun i hi ↦ hs' i <| Finset.mem_cons_of_mem hi
