omega_thirty
plain-language theorem explainer
The declaration establishes that 30 has exactly three distinct prime factors. Number theorists verifying small instances of arithmetic functions would cite this when checking base cases for prime-counting identities. The proof is a direct native computation that evaluates the definition of omega without lemmas or hypotheses.
Claim. $ω(30) = 3$, where $ω(n)$ counts the distinct prime factors of the positive integer $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The sibling definitions introduce bigOmega (total prime factors with multiplicity) and related Möbius properties such as μ(n) = 0 when n is not squarefree. This theorem sits in the NumberTheory.Primes layer that prepares basic facts before Dirichlet inversion or series arguments.
proof idea
One-line wrapper that applies native_decide to evaluate the equality by direct native computation of the omega definition on the constant 30.
why it matters
It supplies a concrete verified instance for the distinct-prime-count function inside the arithmetic-functions module. No downstream theorems are recorded, so it functions as a basic computational anchor rather than feeding a larger chain. Within the Recognition Science formalization it supports exact small-case checks needed for later number-theoretic constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.