bigOmega_onehundredtwenty
plain-language theorem explainer
The theorem states that the total number of prime factors of 120, counted with multiplicity, equals 5. Number theorists using arithmetic functions in the Recognition Science setting would cite this evaluation when checking explicit factorizations such as 2 cubed times 3 times 5. The proof is a direct computational check that applies the native_decide tactic to the definition of the big omega function.
Claim. $Ω(120) = 5$, where $Ω(n)$ denotes the total number of prime factors of $n$ counted 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 the one that counts prime factors. The upstream definition identifies bigOmega with the cardinality of the multiset of prime factors, written as ArithmeticFunction.cardFactors. This places the result in a section focused on basic arithmetic tools that can later support Dirichlet inversion or squarefree checks.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the equality directly from the definition of bigOmega.
why it matters
The result supplies a concrete numerical checkpoint for the big omega function inside the primes arithmetic module. It has no listed downstream uses and does not connect to the forcing chain or phi-ladder steps. The declaration therefore functions as a verified computational fact rather than a structural lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.