prime_onethousandninetythree
plain-language theorem explainer
1093 is established as a prime in the natural numbers and identified as the first Wieferich prime. Number theorists working with arithmetic functions or testing Möbius inversion on small primes would cite this fact. The proof is a one-line native_decide computation that directly checks the primality predicate.
Claim. The natural number $1093$ satisfies the primality predicate, i.e., it is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Statements remain minimal until Dirichlet algebra layers are added. Prime is the local alias for the standard primality predicate on natural numbers.
proof idea
The proof is a one-line wrapper that applies native_decide to confirm 1093 meets the primality definition by direct computation.
why it matters
This supplies a concrete verified prime for evaluations inside the arithmetic functions module. It populates basic facts for Möbius and related functions without shown downstream use. No link to the Recognition Science forcing chain or constants appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.