cardDistinctFactors — Mathlib

English

ω(n) equals the number of distinct prime factors of n; equivalently ω(n) is the length of the deduplicated prime factors list.

Русский

ω(n) равно числу различных простых делителей числа n; эквивалентно длине списка простых делителей без дубликатов.

LaTeX

$$$$\omega(n) = |\{ p : p \mid n, p \text{ prime} \}| = \text{length of } n^{\prime}\!_\text{primeFactorsList}.$$$$

Lean4

/-- `ω n` is the number of distinct prime factors of `n`. -/
def cardDistinctFactors : ArithmeticFunction ℕ :=
  ⟨fun n => n.primeFactorsList.dedup.length, by simp⟩

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