bigOmega_twothousandthreehundredten
plain-language theorem explainer
The declaration establishes that the total number of prime factors of 2310 counted with multiplicity equals 5. Number theorists using arithmetic functions in the Recognition Science setting would cite this concrete evaluation when checking small integers. The proof is a one-line wrapper that invokes native_decide to compute the value directly from the cardFactors definition.
Claim. $Ω(2310) = 5$, where $Ω(n)$ is the arithmetic function that counts the prime factors of $n$ with multiplicity.
background
The module provides lightweight wrappers around Mathlib arithmetic functions, starting from the Möbius function and including the bigOmega abbreviation. bigOmega is defined as ArithmeticFunction.cardFactors, which returns the total number of prime factors counted with multiplicity. This theorem belongs to the NumberTheory.Primes.ArithmeticFunctions module, which supplies concrete evaluations to support prime-related work in the framework. It depends on the bigOmega abbreviation from the same file.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate bigOmega on the constant 2310.
why it matters
This supplies a specific numerical instance inside the arithmetic functions library that supports prime factor counts in the Recognition Science number theory layer. It fills a concrete slot in the primes module even though no downstream uses are recorded. The result is consistent with the framework's pattern of verifying small-integer properties that feed into larger structures such as squarefree checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.