emirp_onehundredthirteen
plain-language theorem explainer
113 and its reversal 311 are both prime and distinct. Number theorists checking concrete emirp instances or verifying small prime pairs would cite the fact. The proof is a direct native_decide computation that evaluates the three conjuncts.
Claim. $113$ is prime, $311$ is prime, and $113$ is distinct from $311$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard predicate Nat.Prime on natural numbers. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added later once interfaces stabilize.
proof idea
One-line wrapper that invokes the native_decide tactic to compute the truth value of the conjunction of the two primality statements and the inequality.
why it matters
The declaration supplies a verified emirp pair inside the primes section. No parent theorems or downstream uses are recorded, so it functions as a concrete numerical checkpoint rather than a link in a larger chain. It sits alongside Möbius and big-Omega definitions but does not interact with them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.