prime_onehundredninetynine
plain-language theorem explainer
199 is shown to be a prime natural number. Researchers evaluating arithmetic functions such as the Möbius function at small prime arguments would cite this fact. The proof reduces to a single native decision procedure that settles the primality claim computationally.
Claim. The natural number $199$ is prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. Prime is the transparent alias for the standard primality predicate on natural numbers. The local setting prepares for Dirichlet algebra and inversion once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to resolve the primality statement.
why it matters
This supplies a concrete prime instance that can support arithmetic function evaluations in the NumberTheory.Primes layer. It aligns with sibling results such as mobius_prime for handling primes under the Möbius function. No direct link to the Recognition Science forcing chain or constants appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.