omega_def
plain-language theorem explainer
Equating the omega arithmetic function to the count of distinct prime factors aligns a custom wrapper with Mathlib's standard implementation. Number theorists simplifying expressions that involve ω(n) would cite this equivalence for rewriting rules. The proof applies reflexivity to match the two sides exactly.
Claim. Let ω denote the arithmetic function that returns the number of distinct prime factors of its argument. Then ω equals the function cardDistinctFactors, where cardDistinctFactors(n) is the cardinality of the set of distinct primes dividing n.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to related maps such as omega and bigOmega. Local conventions treat these as elements of ArithmeticFunction Nat, with omega tracking distinct prime factors while bigOmega tracks total factors with multiplicity. The setting prepares basic interfaces for later Dirichlet inversion once the core definitions stabilize.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity to equate the two sides of the definition.
why it matters
This simp lemma supplies a rewriting rule for the number of distinct prime factors inside the Recognition Science number-theory layer. It supports downstream arithmetic manipulations that may feed into prime-distribution arguments, though no parent theorems are recorded yet. The declaration sits among siblings that handle squarefree detection and Möbius inversion, consistent with the module's focus on foundational arithmetic tools.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.