bigOmega_fortyfive
plain-language theorem explainer
bigOmega_fortyfive asserts that the total number of prime factors of 45 counted with multiplicity equals 3. Number theorists consulting the Recognition Science arithmetic functions library cite this for quick evaluations of Ω at small composite numbers. The proof reduces to a native decision procedure that confirms the factorization 45 = 3² × 5.
Claim. $Ω(45) = 3$, 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 the bigOmega function. Upstream, bigOmega is defined as the arithmetic function cardFactors, which returns the total number of prime factors counted with multiplicity. The local setting keeps statements minimal to allow later layering of Dirichlet algebra.
proof idea
The proof applies the native_decide tactic in a single step to evaluate the arithmetic function at the concrete input 45.
why it matters
The result provides a verified constant in the arithmetic functions module. It supports basic number theoretic calculations within the Recognition Science framework, though no immediate downstream uses are recorded. It aligns with the prime factorization footholds needed before deeper connections to inversion formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.