radical_dvd_radical — Mathlib

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

Похожие утверждения