divRadical — Mathlib

English

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

Русский

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

LaTeX

$$$\text{IsCoprime}(\operatorname{divRadical}(a), \operatorname{divRadical}(b))$$$

Lean4

theorem _root_.IsCoprime.divRadical {a b : E} (h : IsCoprime a b) : IsCoprime (divRadical a) (divRadical b) :=
  by
  rw [← radical_mul_divRadical (a := a)] at h
  rw [← radical_mul_divRadical (a := b)] at h
  exact h.of_mul_left_right.of_mul_right_right

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