bigOmega_prime_pow
plain-language theorem explainer
Ω(p^k) equals k for any prime p and natural number k. Researchers reducing sums or products over prime powers in arithmetic-function identities would invoke this fact. The argument lifts the local Prime predicate to Nat.Prime via prime_iff, performs case analysis on the exponent, and dispatches the zero case with bigOmega_apply while the positive case follows from the standard cardFactors_apply_prime_pow lemma.
Claim. Let $p$ be a prime number and $k$ a nonnegative integer. Then the arithmetic function Ω satisfies Ω(p^k) = k, where Ω(n) counts the prime factors of n with multiplicity.
background
bigOmega is the arithmetic function that returns the length of the prime-factors list of its argument, hence the total number of prime factors counted with multiplicity. Prime is the repository alias for Nat.Prime. The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to Ω and ω. Upstream, bigOmega_apply states that Ω(n) equals the length of n.primeFactorsList. The proof also relies on the standard fact that the card-factors function applied to a prime power equals the exponent.
proof idea
The proof first converts Prime p into Nat.Prime p by applying the equivalence prime_iff. It then performs case analysis on k. The zero case is immediate from bigOmega_apply. The successor case is obtained directly by applying ArithmeticFunction.cardFactors_apply_prime_pow to the Nat.Prime witness.
why it matters
This identity supplies the evaluation of Ω on prime powers, a prerequisite for any later Dirichlet-convolution or inversion work inside the Recognition Science number-theory layer. No downstream uses are recorded yet, but the result closes the standard base case needed for prime-power reductions in arithmetic-function identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.