prime_threehundredseventeen
plain-language theorem explainer
317 is established as prime by direct computational check. Number theorists using Möbius inversion or arithmetic functions in the Recognition Science setting would cite this when verifying small primes for factorization identities. The proof is a one-line term that invokes native_decide on the Nat.Prime predicate.
Claim. $317$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ. Prime is the transparent alias for Nat.Prime. Upstream results include the Prime abbrev from Basic and several 'is' structures from foundation modules that certify collision-free or tautological properties without new axioms.
proof idea
The proof is a one-line term that applies native_decide to discharge the primality goal for 317.
why it matters
This supplies a verified small prime for arithmetic-function calculations in the NumberTheory.Primes submodule. It supports the Möbius footholds described in the module documentation. No downstream uses are recorded, leaving open its role in larger inversion or prime-counting steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.