bigOmega_twelve
plain-language theorem explainer
bigOmega_twelve asserts that the total number of prime factors of 12 counted with multiplicity equals 3. Number theorists verifying small cases for arithmetic functions would cite this equality when checking base values ahead of Möbius inversion or Dirichlet series work. The proof reduces to a single native_decide call that evaluates the definition of bigOmega directly on the constant 12.
Claim. $Ω(12) = 3$, where $Ω(n)$ denotes the arithmetic function that counts the prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function and extending to the big omega function. bigOmega is introduced as the abbreviation ArithmeticFunction.cardFactors, which tallies all prime factors of its argument with multiplicity. The local setting keeps statements minimal so that deeper Dirichlet algebra can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the equality from the definition of bigOmega.
why it matters
This declaration supplies a concrete base-case check inside the arithmetic functions module. It supports the module's stated goal of stabilizing interfaces for Möbius and related functions before layering further structure. No downstream uses are recorded, so the result functions as an isolated verification rather than a step toward a larger theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.