squarefree_iff_factorization_le_one

English

For nonzero n, Squarefree n holds iff for every p, n.factorization p ≤ 1.

Русский

Для ненулевого n квадратность n эквивалентна тому, что для каждого p n.factorization p ≤ 1.

LaTeX

$$$n \\neq 0 \\rightarrow (Squarefree(n) \\iff \\forall p, n.factorization(p) \\le 1)$$$

Lean4

theorem squarefree_iff_factorization_le_one {n : ℕ} (hn : n ≠ 0) : Squarefree n ↔ ∀ p, n.factorization p ≤ 1 :=
  ⟨fun hn => hn.natFactorization_le_one, squarefree_of_factorization_le_one hn⟩

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