squarefree_of_factorization_le_one

English

If n ≠ 0 and for all p, n.factorization p ≤ 1, then n is squarefree.

Русский

Если n ≠ 0 и для всех p n.factorization p ≤ 1, то n квадратносвободно.

LaTeX

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

Lean4

theorem squarefree_of_factorization_le_one {n : ℕ} (hn : n ≠ 0) (hn' : ∀ p, n.factorization p ≤ 1) : Squarefree n :=
  by
  rw [squarefree_iff_nodup_primeFactorsList hn, List.nodup_iff_count_le_one]
  intro a
  rw [primeFactorsList_count_eq]
  apply hn'

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