palindromic_prime_two
plain-language theorem explainer
The declaration states that 2 is prime and therefore a single-digit palindromic prime in base 10. Number theorists referencing base cases for arithmetic functions or prime lists would cite it. The proof is a one-line native decision procedure that directly confirms primality.
Claim. The integer $2$ is a prime number and hence a palindromic prime in base ten.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function before deeper Dirichlet algebra is added. The local setting treats statements as thin interfaces. The Prime predicate is the transparent alias for the standard Nat.Prime predicate on natural numbers.
proof idea
The proof is a one-line term that applies native_decide to verify that 2 satisfies the primality predicate.
why it matters
The result supplies the smallest prime as a base fact inside the primes section of the arithmetic-functions module. It supports later definitions such as Möbius applied to primes. No downstream theorems are recorded and the declaration touches none of the Recognition Science forcing chain steps or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.