palindromic_prime_onehundredone
plain-language theorem explainer
101 is established as a prime number. Number theorists building arithmetic functions or checking small cases in the Recognition Science number theory layer would cite this for basic verification. The proof is a one-line computational decision via native_decide that confirms the predicate without manual unfolding or lemmas.
Claim. $101$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function as the initial interface before deeper Dirichlet algebra. Prime is the transparent alias for Nat.Prime supplied in the sibling Basic file. This theorem sits inside the primes subsection and uses only that alias together with the native decision procedure.
proof idea
The proof is a one-line wrapper that applies native_decide to the primality predicate on 101.
why it matters
The declaration supplies a verified concrete prime instance inside the arithmetic functions module. It supports the lightweight scaffolding described in the module documentation but has no downstream uses and does not engage the forcing chain, RCL, or RS-native constants. It closes a basic fact without touching open questions in the primes development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.