bigOmega_mul
plain-language theorem explainer
Ω counting prime factors with multiplicity satisfies Ω(mn) = Ω(m) + Ω(n) for nonzero natural numbers m and n. Number theorists handling arithmetic functions cite this when proving complete multiplicativity of the Liouville function. The proof is a one-line wrapper that unfolds the abbreviation and applies the Mathlib cardFactors_mul lemma.
Claim. Let $Ω(k)$ denote the number of prime factors of the natural number $k$ counted with multiplicity. For nonzero natural numbers $m$ and $n$, $Ω(mn) = Ω(m) + Ω(n)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as a foothold for Dirichlet inversion. bigOmega is introduced as the abbreviation ArithmeticFunction.cardFactors, which encodes the standard Ω function: the sum of exponents in the prime factorization of its argument. The local setting keeps statements minimal so that deeper multiplicative algebra can be added once interfaces stabilize.
proof idea
This is a one-line wrapper. It unfolds the abbreviation bigOmega via simp only [bigOmega] and invokes the Mathlib lemma ArithmeticFunction.cardFactors_mul under the nonzero hypotheses hm and hn.
why it matters
The result is invoked in the proof of liouville_mul to establish that the Liouville function is completely multiplicative. Within the Recognition Science framework it supplies a basic identity on prime factor counts needed for handling factorizations that appear in the phi-ladder and related arithmetic constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.