squarefree_natAbs — Mathlib

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]

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