radical_mul — Mathlib

English

If a and b are coprime, then radical(ab) = radical(a) radical(b).

Русский

Если a и b взаимно просты, то radical(ab) = radical(a) radical(b).

LaTeX

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

Lean4

/-- Radical is multiplicative for relatively prime elements. -/
theorem radical_mul (hc : IsRelPrime a b) : radical (a * b) = radical a * radical b :=
  by
  simp_rw [radical]
  rw [primeFactors_mul_eq_disjUnion hc, Finset.prod_disjUnion (disjoint_primeFactors hc)]

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