prime_onehundredseven
plain-language theorem explainer
107 is a prime number. Number theorists working with arithmetic functions or small-prime instances would cite this for direct verification inside larger calculations. The proof is a one-line wrapper that applies the native_decide tactic to resolve the statement by computation.
Claim. $107$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. The local setting keeps statements basic so that deeper Dirichlet algebra and inversion can be added once interfaces stabilize. The sole upstream dependency is the transparent alias Prime, defined as the standard primality predicate on natural numbers.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the primality predicate directly.
why it matters
This supplies a concrete verified prime inside the arithmetic-functions module. It stands as a basic number-theoretic fact available for any downstream use of primes in Möbius or related calculations, though no such uses are currently recorded. It does not touch the forcing chain or Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.