semiprime_twentytwo
plain-language theorem explainer
22 equals the product of the distinct primes 2 and 11 and therefore satisfies the semiprime predicate. Number theorists checking small instances of arithmetic functions would cite this as a concrete base case. The proof reduces the claim to a single native decision procedure on the bigOmega definition.
Claim. The integer 22 satisfies $Ω(22)=2$, where $Ω$ counts the total number of prime factors with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The predicate isSemiprime is defined by isSemiprime n := bigOmega n = 2. This theorem supplies a concrete instance for n=22, which factors as 2×11.
proof idea
one-line wrapper that applies native_decide to the isSemiprime definition.
why it matters
This declaration provides a verified base case for semiprime numbers inside the arithmetic functions module. It supports downstream checks in prime-related computations within the Recognition framework, though no immediate parent theorem is listed. It aligns with the lightweight approach to number-theoretic foundations before layering Dirichlet algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.