bigOmega
plain-language theorem explainer
bigOmega defines the arithmetic function Ω(n) counting all prime factors of n with multiplicity. Number theorists cite it for prime factorization counts in arithmetic function calculations. The declaration is a direct one-line abbreviation aliasing Mathlib's cardFactors.
Claim. Let Ω be the arithmetic function on natural numbers such that Ω(n) equals the total number of prime factors of n counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. bigOmega is introduced as the cardFactors function, which sums the exponents in the prime factorization of its argument. The local theoretical setting keeps statements minimal so that Dirichlet convolution and inversion can be added once the basic interfaces are stable.
proof idea
This is a one-line wrapper that directly aliases ArithmeticFunction.cardFactors.
why it matters
It supplies the base definition for Ω(n) that feeds the 32 downstream results, including bigOmega_apply (which equates Ω(n) to the length of the primeFactorsList) and concrete evaluations such as bigOmega_eight and bigOmega_eighthundredforty. In the Recognition framework it anchors prime-counting steps inside the NumberTheory.Primes module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.