English
If a finite set of elements f(i) are pairwise coprime and each f(i) is squarefree, then their product is squarefree.
Русский
Если конечное множество элементов f(i) попарно взаимно простое и каждый f(i) квадратно свободен, то их произведение квадратно свободно.
LaTeX
$$$\bigl(\forall i, i\in s \rightarrow \mathrm{Squarefree}(f(i))\bigr) \wedge \mathrm{Set.Pairwise}(s, \mathrm{IsRelPrime}(f)) \rightarrow \mathrm{Squarefree}\bigl(\prod_{i\in s} f(i)\bigr)$$$
Lean4
theorem dvd_of_squarefree_of_mul_dvd_mul_right (hx : Squarefree x) (h : d * d ∣ x * y) : d ∣ y :=
by
nontriviality R
obtain ⟨a, b, ha, hb, eq⟩ := exists_dvd_and_dvd_of_dvd_mul h
replace ha : Squarefree a := hx.squarefree_of_dvd ha
obtain ⟨c, hc⟩ : a ∣ d := ha.isRadical 2 d ⟨b, by rw [sq, eq]⟩
rw [hc, mul_assoc, (mul_right_injective₀ ha.ne_zero).eq_iff] at eq
exact dvd_trans ⟨c, by rw [hc, ← eq, mul_comm]⟩ hb
