bigOmega_factorial_three
plain-language theorem explainer
The declaration establishes that the total number of prime factors of 3 factorial, counted with multiplicity, equals 2. Number theorists checking small cases of arithmetic functions would cite this when validating base computations. The proof proceeds by direct evaluation via native decision procedures rather than inductive argument.
Claim. $Ω(3!) = 2$, where $Ω(n)$ counts the prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to related maps such as bigOmega. bigOmega is the arithmetic function that returns the total number of prime factors counted with multiplicity, implemented directly as cardFactors. This definition supplies the concrete operation used in the present statement and anchors subsequent prime-counting identities.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the factorial and its prime factorization directly.
why it matters
The result supplies a verified base case inside the arithmetic-functions layer of the primes module. It supports incremental construction of number-theoretic tools that may later feed into Recognition Science calculations involving prime ladders, though no downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.