semiprime_twentyone
plain-language theorem explainer
21 qualifies as semiprime because its prime factorization 3 × 7 yields exactly two prime factors counted with multiplicity. Number theorists verifying small cases in arithmetic function tables or semiprime classifications would reference this check. The proof reduces the claim to direct evaluation of bigOmega via native_decide.
Claim. $21$ is semiprime, i.e., the total number of prime factors of $21$ counted with multiplicity equals two: $Ω(21) = 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The sibling definition isSemiprime states that a natural number n is semiprime precisely when bigOmega n = 2, where bigOmega counts the total number of prime factors with multiplicity. This theorem supplies the concrete instance for n = 21, which factors as 3 × 7.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate isSemiprime 21 by computing bigOmega 21 and confirming equality to 2.
why it matters
The declaration supplies a verified base case for the semiprime predicate inside the arithmetic-functions module. It supports the number-theory layer of the Recognition Science framework that later feeds into prime-related constructions, though no downstream uses are recorded. The module documentation positions such checks as preparatory scaffolding before deeper Dirichlet inversion is added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.