emirp_thirteen
plain-language theorem explainer
The statement confirms that 13 and its digit reversal 31 are distinct primes. Researchers checking small emirp pairs in number-theoretic foundations would reference this case. The verification proceeds by direct computational resolution of the primality predicates and inequality.
Claim. $13$ is prime, $31$ is prime, and $13$ differs from $31$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local setting keeps statements minimal to support later Dirichlet inversion once interfaces stabilize. Prime is the module-local abbreviation for natural-number primality.
proof idea
A one-line term proof applies native_decide to evaluate the conjunction of the two primality checks and the inequality.
why it matters
The declaration supplies a concrete emirp example inside the number-theory layer. It has no downstream uses in the current graph and does not feed any parent theorem. The fact sits among prime foundations without direct ties to the forcing chain or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.