cardDistinctFactors_eq_cardFactors_iff_squarefree

English

For n ≠ 0, ω(n) = Ω(n) if and only if n is squarefree.

Русский

Для n ≠ 0 условие ω(n) = Ω(n) эквивалентно тому, что n квадратно свободно.

LaTeX

$$$$\omega(n) = \Omega(n) \quad \text{iff} \quad \text{Squarefree}(n)$$$$

Lean4

theorem cardDistinctFactors_eq_cardFactors_iff_squarefree {n : ℕ} (h0 : n ≠ 0) : ω n = Ω n ↔ Squarefree n :=
  by
  rw [squarefree_iff_nodup_primeFactorsList h0, cardDistinctFactors_apply]
  constructor <;> intro h
  · rw [← n.primeFactorsList.dedup_sublist.eq_of_length h]
    apply List.nodup_dedup
  · simp [h.dedup, cardFactors]

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