bigOmega_one
plain-language theorem explainer
Ω(1) evaluates to zero under the total prime factor count with multiplicity. Number theorists working with arithmetic functions cite this as the base case for Ω on the unit. The proof reduces immediately via simplification on the apply lemma for the definition.
Claim. $Ω(1) = 0$, where $Ω(n)$ denotes the total number of prime factors of $n$ counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and extending to Ω. bigOmega is the abbreviation for the arithmetic function that counts prime factors with multiplicity. The upstream lemma bigOmega_apply states that Ω(n) equals the length of the list of prime factors of n.
proof idea
The proof is a one-line wrapper that applies bigOmega_apply to the case n=1.
why it matters
This base case anchors the arithmetic functions module for primes, which supports number-theoretic scaffolding in the Recognition framework. It aligns with the self-reference structures from UniversalForcingSelfReference by supplying a concrete evaluation at the unit. No direct downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.