English
Squarefree (x ⋅ y) iff IsRelPrime x y and Squarefree x and Squarefree y.
Русский
Squarefree(xy) эквивалентно: x и y взаимно просты и x и y квадратно свободны.
LaTeX
$$$\mathrm{Squarefree}(\mathrm{instHMul.hMul}(x,y)) \iff \mathrm{IsRelPrime}(x,y) \land \mathrm{Squarefree}(x) \land \mathrm{Squarefree}(y)$$$
Lean4
/-- `x * y` is square-free iff `x` and `y` have no common factors and are themselves square-free. -/
theorem squarefree_mul_iff : Squarefree (x * y) ↔ IsRelPrime x y ∧ Squarefree x ∧ Squarefree y :=
⟨fun h ↦ ⟨IsRelPrime.of_squarefree_mul h, h.of_mul_left, h.of_mul_right⟩, fun ⟨hp, sqx, sqy⟩ _ dvd ↦
hp (sqy.dvd_of_squarefree_of_mul_dvd_mul_left dvd) (sqx.dvd_of_squarefree_of_mul_dvd_mul_right dvd)⟩
