palindromic_prime_eleven
plain-language theorem explainer
Eleven is established as a prime number in the natural numbers. Number theorists working in the Recognition Science arithmetic setting would cite this when verifying small palindromic cases for Möbius-related computations. The verification reduces directly to a native decision procedure that confirms the primality property computationally.
Claim. $11$ is a prime number in the natural numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the repo-local alias for the standard predicate on natural numbers. This theorem appears in the primes section of the arithmetic functions file, where statements remain minimal to allow later layering of Dirichlet algebra.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the primality goal for 11.
why it matters
This supplies a basic verified fact for the palindromic prime 11 that the Recognition Science framework marks as relevant. It supports the arithmetic functions module but feeds no downstream theorems in the current graph. The placement aligns with the module's focus on small-integer cases that can anchor later prime and squarefree properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.