semiprime_fiftyseven
plain-language theorem explainer
The declaration shows that 57 equals 3 times 19 and therefore meets the semiprime condition that the total number of prime factors counted with multiplicity equals exactly two. Number theorists inside the Recognition Science arithmetic layer would reference the result when verifying small composite cases for Möbius and bigOmega properties. The proof reduces to a single native_decide call that evaluates the isSemiprime definition directly on the concrete input.
Claim. $57 = 3 × 19$ is semiprime, i.e., the total number of prime factors of 57 counted with multiplicity equals 2.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. A number n is semiprime precisely when its bigOmega value, the total prime factor count with multiplicity, equals exactly 2. The isSemiprime definition implements this check as bigOmega n = 2.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the isSemiprime predicate on the concrete input 57.
why it matters
This concrete instance supports the arithmetic functions module in the NumberTheory.Primes section. It fills a basic check for semiprimes without feeding into any downstream theorems in the current graph. It aligns with the lightweight approach to Dirichlet algebra described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.