prime_threehundredthirteen
plain-language theorem explainer
313 is a prime natural number. Number theorists working with arithmetic functions or small-prime inputs to Möbius inversions in the Recognition Science setting would cite this fact for verification steps. The proof is a one-line native decision that evaluates the primality predicate directly from its definition.
Claim. $313$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the repo-local transparent alias for the standard predicate Nat.Prime on natural numbers. This theorem supplies a concrete small-prime instance inside that arithmetic-functions context.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the primality statement.
why it matters
The declaration supplies a verified prime fact inside the arithmetic-functions module that supports Möbius and related number-theoretic constructions. No downstream uses are recorded. It aligns with the need for exact small-integer facts when building toward Recognition Science number-theoretic results such as prime ladders or inversion formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.