palindromic_prime_onehundredeightyone
plain-language theorem explainer
The theorem asserts that 181 is a prime number and notes its palindromic form. Number theorists working with small primes or arithmetic function examples could cite this concrete case. The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the primality predicate directly.
Claim. The natural number 181 is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This theorem sits inside that file as a basic primality fact. Upstream, Prime is a transparent alias for Nat.Prime.
proof idea
The proof is a one-line wrapper applying the native_decide tactic to confirm that 181 satisfies the primality condition.
why it matters
This supplies a specific palindromic prime example inside the arithmetic functions module. It feeds no downstream theorems. Within the Recognition framework it offers a basic number-theoretic instance, though it touches none of the T0-T8 forcing chain, RCL, or phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.