emirp_thirtyseven
plain-language theorem explainer
The declaration asserts that 37 and its digit reversal 73 are both prime and distinct. Number theorists examining emirp examples or reversal-symmetric primes in the Recognition Science setting would reference this instance. The proof reduces to a single native_decide tactic that evaluates the primality predicates and inequality directly.
Claim. Both $37$ and its digit reversal $73$ are prime numbers, and $37 ≠ 73$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This theorem appears among prime-related facts in the NumberTheory.Primes section. The Prime predicate is the repository-local alias for Mathlib’s standard Nat.Prime predicate, kept transparent.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the conjunction of primality for 37, primality for 73, and their inequality.
why it matters
This supplies a concrete numerical example of an emirp in the arithmetic functions module, aligning with Recognition Science interest in specific prime structures. It does not feed any downstream theorems in the current dependency graph. The emirp property touches the framework’s attention to reversal patterns without invoking the Möbius or big-Omega machinery present in sibling declarations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.