bigOmega_threehundredsixty
plain-language theorem explainer
The theorem establishes that the total number of prime factors of 360, counted with multiplicity, equals 6. Number theorists verifying factorizations or testing arithmetic function implementations would cite this concrete case. The proof is a one-line native_decide application that evaluates the definition directly.
Claim. $Ω(360) = 6$, where $Ω(n)$ denotes the total number of prime factors of $n$ counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function and extending to related functions. The upstream bigOmega is defined as the arithmetic function cardFactors, described as the number of prime factors (with multiplicity) — Ω(n). This occurs in the local setting of basic interfaces for Dirichlet algebra and inversion.
proof idea
The proof is a one-line term that invokes native_decide to compute the value of bigOmega 360 from its definition as the cardinality of prime factors.
why it matters
This specific evaluation serves as a concrete test case within the arithmetic functions module, supporting the development of Möbius-related tools. It does not tie into the Recognition Science forcing chain T0-T8, the Recognition Composition Law, or constants such as phi. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.