bigOmega_pow
plain-language theorem explainer
Ω(n^k) equals k times Ω(n) for all natural numbers n and k. Researchers working with completely additive arithmetic functions would cite this when reducing expressions that involve integer powers. The proof is a one-line wrapper that unfolds the bigOmega abbreviation and invokes Mathlib's cardFactors_pow lemma.
Claim. $Ω(n^k) = k ⋅ Ω(n)$ for all natural numbers $n$ and $k$.
background
bigOmega is the abbreviation for ArithmeticFunction.cardFactors, the standard arithmetic function that returns the total number of prime factors of its argument counted with multiplicity. The module supplies thin wrappers around Mathlib's arithmetic-function library, beginning with the Möbius function μ and continuing to related counting functions. The upstream declaration bigOmega simply aliases cardFactors, supplying the conventional Ω notation used throughout the file.
proof idea
The term proof first applies simp only [bigOmega] to replace the abbreviation by cardFactors, then invokes the exact lemma ArithmeticFunction.cardFactors_pow.
why it matters
The identity is the standard power rule for the completely additive function Ω and immediately precedes the definition of the Liouville function λ(n) = (-1)^Ω(n) in the same file. It supplies a basic algebraic fact needed for any later manipulation of Ω in the arithmetic-functions layer of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.