English
Absolute value does not affect squarefreeness: for any integer n, Squarefree(n.natAbs) ↔ Squarefree(n).
Русский
Модуль числа не влияет на квадратноcвободность: для любого целого n выполняется эквивалентность Squarefree(natAbs(n)) ↔ Squarefree(n).
LaTeX
$$$$ \operatorname{Squarefree}(\operatorname{natAbs}(n)) \iff \operatorname{Squarefree}(n). $$$$
Lean4
@[simp]
theorem squarefree_natAbs {n : ℤ} : Squarefree n.natAbs ↔ Squarefree n := by
simp_rw [Squarefree, natAbs_surjective.forall, ← natAbs_mul, natAbs_dvd_natAbs, isUnit_iff_natAbs_eq, Nat.isUnit_iff]