prime_twohundredninetythree
plain-language theorem explainer
293 is established as a prime number. Number theorists working with arithmetic functions or small-prime verifications would cite it to anchor computations such as Möbius evaluations. The proof is a one-line native_decide application that evaluates the primality predicate by direct computation.
Claim. $293$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Local setting defines Primes as the set of natural numbers satisfying the primality predicate, with Prime as the transparent local alias for that predicate. Upstream results include the Primes set definition and the Prime abbreviation, which this theorem instantiates for the concrete value 293.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the primality predicate for 293 by native computation.
why it matters
This supplies a verified prime fact in the 300s that supports arithmetic-function statements such as Möbius calculations for squarefree integers in the same module. It fills a basic verification step in the NumberTheory.Primes section. The result remains isolated from the Recognition Science forcing chain, phi-ladder, or dimension-forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.