prime_onehundredsixtyseven
plain-language theorem explainer
The declaration asserts that 167 is a prime natural number. Number theorists handling arithmetic functions such as the Möbius function in prime-specific cases would cite this fact when building basic interfaces. The verification proceeds by direct computational check via the native_decide tactic.
Claim. The natural number $167$ is prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. The local setting keeps statements minimal to allow later layering of Dirichlet algebra and inversion once basic interfaces stabilize. The upstream result defines the Prime predicate as the standard primality condition on natural numbers.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to confirm primality of 167 by direct computation.
why it matters
This supplies a concrete prime instance for arithmetic function calculations in the NumberTheory.Primes module. It supports prime cases in Möbius footholds and aligns with Recognition Science use of number-theoretic facts, though no downstream applications are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.