prime_onehundredfiftyseven
plain-language theorem explainer
157 is established as a prime natural number. Researchers applying Möbius or other arithmetic functions to concrete primes in the Recognition Science setting would cite this fact for case handling. The verification reduces directly to a computational decision procedure.
Claim. $157$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function, and keeps statements minimal to permit later addition of Dirichlet inversion. Prime is the transparent alias for the standard predicate on natural numbers. The upstream definition simply re-exports the usual primality condition without additional structure.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the primality claim by direct computation.
why it matters
The result supplies a verified prime instance inside the arithmetic-functions module, supporting prime-specific evaluations of the Möbius function before deeper inversion results are layered on. It sits at the base of the NumberTheory.Primes hierarchy and aligns with the need for concrete facts prior to any connection with the Recognition forcing chain or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.