palindromic_prime_sevenhundredfiftyseven
plain-language theorem explainer
757 is a palindromic prime. Number theorists building arithmetic tools inside Recognition Science would cite this fact when populating concrete integer examples for Möbius and related functions. The proof is a one-line term that invokes native_decide to verify the primality predicate computationally.
Claim. The natural number 757 is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent local alias for the standard primality predicate on natural numbers. The theorem asserts that 757 satisfies this predicate and is documented as palindromic.
proof idea
The proof is a one-line term that applies native_decide to discharge the primality goal for 757.
why it matters
This supplies a verified concrete prime instance inside the arithmetic-functions module that supports Möbius footholds. It contributes to the number-theory layer of Recognition Science without listed downstream uses, serving as a building block for later prime-dependent statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.