squarefree_natCast — Mathlib

English

For n ∈ ℕ, squarefree(n interpreted as an integer) is equivalent to squarefree(n) as a natural number.

Русский

Для n ∈ ℕ квадратность n как целого числа равна квадратности n как натурального числа.

LaTeX

$$$$ \operatorname{Squarefree}(n : \mathbb{Z}) \iff \operatorname{Squarefree}(n). $$$$

Lean4

@[simp]
theorem squarefree_natCast {n : ℕ} : Squarefree (n : ℤ) ↔ Squarefree n := by rw [← squarefree_natAbs, natAbs_natCast]

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