squarefree_iff_nodup_primeFactorsList

English

For n ≠ 0, Squarefree(n) iff n.primeFactorsList.Nodup.

Русский

Для n ≠ 0 верно: квадратно-простой n эквивалентно тому, что список простых делителей n не содержит повторов.

LaTeX

$$$ n \\neq 0 \\Rightarrow \\text{Squarefree}(n) \\iff n.primeFactorsList.Nodup $$$

Lean4

theorem squarefree_iff_nodup_primeFactorsList {n : ℕ} (h0 : n ≠ 0) : Squarefree n ↔ n.primeFactorsList.Nodup :=
  by
  rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0, Nat.factors_eq]
  simp

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