semiprime_ninetyone
plain-language theorem explainer
The declaration verifies that 91 satisfies the semiprime condition by direct evaluation of its prime factorization. Number theorists using arithmetic functions in the Recognition Science number-theory layer would cite this as a concrete check on small integers. The proof reduces to a native decision procedure that computes bigOmega 91 and compares it to 2.
Claim. $91$ is semiprime, i.e., the total number of prime factors of $91$ counted with multiplicity equals $2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to bigOmega. isSemiprime is defined by the equation bigOmega n = 2, where bigOmega counts prime factors with multiplicity. Upstream results supply the isSemiprime definition together with auxiliary structures that guarantee algebraic or collision-free properties in the surrounding foundation modules.
proof idea
The proof is a one-line wrapper that applies native_decide to the boolean expression obtained by substituting 91 into the definition of isSemiprime.
why it matters
This instance supplies a basic semiprime check inside the arithmetic-functions module that supports Möbius-based number theory in the Recognition framework. It fills a concrete verification step for prime-related calculations without feeding any listed downstream theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.