omega_fortyfive
plain-language theorem explainer
ω(45) equals 2 because 45 factors as 3² × 5. Number theorists verifying small arithmetic function values would cite this evaluation when checking base cases for prime-counting routines. The equality follows from a native decision procedure that evaluates the definition directly on the concrete integer.
Claim. The number of distinct prime factors of 45 is 2, i.e., $ω(45) = 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The omega function counts distinct prime divisors of a positive integer. This theorem evaluates the function at the specific input 45 with no upstream lemmas required.
proof idea
The proof is a one-line term that invokes native_decide to resolve the equality by direct computation of the omega definition.
why it matters
It supplies a verified concrete value inside the arithmetic functions module that supports Möbius footholds and prime-related properties. No parent theorems or downstream uses appear in the current graph, leaving the result as an isolated base-case check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.