squarefree_iff_prime_squarefree — Mathlib

English

Let n be a natural number. Then n is squarefree if and only if for every prime x, x^2 does not divide n.

Русский

Пусть n — натуральное число. Тогда n является квадратносвободным тогда и только тогда, когда для любого простого числа x выполняется, что x^2 не делит n.

LaTeX

$$$\\\\operatorname{Squarefree}(n) \\\\iff \\\\forall x \\, (\\\\operatorname{Prime}(x) \\\\rightarrow \\\\neg (x^2 \\\\mid n))$$$

Lean4

theorem squarefree_iff_prime_squarefree {n : ℕ} : Squarefree n ↔ ∀ x, Prime x → ¬x * x ∣ n :=
  squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible ⟨_, prime_two⟩

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