divRadical_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem divRadical_mul (hab : IsCoprime a b) : divRadical (a * b) = divRadical a * divRadical b :=
  by
  symm; apply eq_divRadical
  rw [UniqueFactorizationMonoid.radical_mul hab.isRelPrime]
  rw [mul_mul_mul_comm, radical_mul_divRadical, radical_mul_divRadical]

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