English
If a divides b and b ≠ 0, then radical(a) divides radical(b).
Русский
Если a делит b и b ≠ 0, то radical(a) делит radical(b).
LaTeX
$$$a \mid b \quad \wedge \quad b \neq 0 \implies \operatorname{radical}(a) \mid \operatorname{radical}(b)$$$
Lean4
/-- If `a` divides `b`, then the radical of `a` divides the radical of `b`. The theorem requires
that `b ≠ 0`, since `radical 0 = 1` but `a ∣ 0` holds for every `a`. -/
theorem radical_dvd_radical (h : a ∣ b) (hb₀ : b ≠ 0) : radical a ∣ radical b :=
by
obtain rfl | ha₀ := eq_or_ne a 0
· simp
rw [dvd_iff_normalizedFactors_le_normalizedFactors ha₀ hb₀] at h
rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors]
exact Multiset.subset_of_le h