bigOmega_thirty
plain-language theorem explainer
bigOmega_thirty asserts that the total number of prime factors of 30 counted with multiplicity equals three. Number theorists verifying small cases inside arithmetic function libraries would cite it for concrete checks. The proof applies native_decide to evaluate the equality directly from the cardFactors definition.
Claim. $Ω(30) = 3$, where $Ω(n)$ denotes the total number of prime factors of $n$ counted with multiplicity.
background
In the arithmetic functions module, bigOmega is the function that returns the total number of prime factors with multiplicity for any natural number. The module supplies lightweight wrappers around Mathlib's arithmetic library, beginning with the Möbius function and related maps, to support later Dirichlet algebra. The upstream definition sets bigOmega as the abbreviation ArithmeticFunction.cardFactors.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to compute the equality from the cardFactors definition.
why it matters
This declaration supplies a concrete numerical check inside the NumberTheory.Primes.ArithmeticFunctions module. It has no downstream uses recorded. It anchors basic prime-counting facts without reference to the forcing chain, the phi-ladder, or Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.