radical_mul_dvd — Mathlib

English

For any a,b, radical(a b) divides radical(a) radical(b).

Русский

Для любых a,b, radical(ab) делит radical(a) radical(b).

LaTeX

$$$\operatorname{radical}(a b) \mid \operatorname{radical}(a) \cdot \operatorname{radical}(b)$$$

Lean4

theorem radical_mul_dvd : radical (a * b) ∣ radical a * radical b := by
  classical
  obtain rfl | ha := eq_or_ne a 0
  · simp
  obtain rfl | hb := eq_or_ne b 0
  · simp
  nontriviality M
  simp [radical_dvd_iff_primeFactors_subset, primeFactors_mul_eq_union, primeFactors_mul_eq_union ha hb,
    primeFactors_radical]

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