isRadical — Mathlib

English

If x ≠ 0 and x is radical, then x is squarefree.

Русский

Если x ≠ 0 и x радикальнo, то x квадратно свободно.

LaTeX

$$$x \\neq 0 \\;\Rightarrow\\; {\\text{IsRadical}(x) } \\Rightarrow \\; \\text{Squarefree}(x).$$$

Lean4

theorem isRadical {x : R} (hx : Squarefree x) : IsRadical x :=
  (isRadical_iff_pow_one_lt 2 one_lt_two).2 fun y hy ↦
    by
    obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul (sq y ▸ hy)
    exact (IsRelPrime.of_squarefree_mul hx).mul_dvd ha hb

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