bigOmega_factorial_four
plain-language theorem explainer
Ω(4!) equals 4, where Ω counts prime factors with multiplicity. Number theorists checking small cases of arithmetic functions on factorials would cite this verification. The proof is a direct native computation of the value.
Claim. Let $Ω(n)$ be the total number of prime factors of $n$ counted with multiplicity. Then $Ω(4!) = 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to Ω(n). bigOmega is the abbrev for ArithmeticFunction.cardFactors, the standard Ω function. This theorem is a basic verification among small natural-number cases in the primes section.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the equality by direct computation.
why it matters
This supplies a concrete check for bigOmega on 4! inside the arithmetic-functions module. It supports downstream prime-related computations, though no parent theorem or direct tie to the Recognition forcing chain appears in the supplied results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.