chen_prime_nineteen
plain-language theorem explainer
19 is prime while 21 factors as 3 times 7, satisfying the semiprime condition. Number theorists examining Chen primes or small-gap phenomena would reference this explicit case. The proof reduces to a single native decision procedure that evaluates both predicates by direct computation.
Claim. $19$ is prime and the total number of prime factors of $21$, counted with multiplicity, equals two.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the repository alias for the standard primality predicate on natural numbers. isSemiprime n holds precisely when the big-Omega function of n equals 2, i.e., n has exactly two prime factors counting multiplicity.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the two predicates.
why it matters
The declaration records a verified Chen-prime instance inside the arithmetic-functions library. It supplies a concrete data point for any later work on prime-factor counts or gap properties that may feed into Recognition Science number-theoretic scaffolding, though no downstream theorem currently cites it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.