prime_onehundredninetythree
plain-language theorem explainer
193 is established as prime. Number theorists applying Möbius inversion or squarefree checks to small integers would reference this for verified input. The proof is a direct computational decision via native_decide on the Nat.Prime predicate.
Claim. The natural number 193 is prime, i.e., $193$ satisfies the predicate $n$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias Nat.Prime n. This instance appears among sibling results such as mobius_prime and mobius_apply_of_squarefree that rely on concrete prime inputs.
proof idea
One-line wrapper that invokes the native_decide tactic to evaluate the primality predicate by direct computation.
why it matters
Supplies a verified small prime for downstream arithmetic-function lemmas such as mobius_prime. It closes a basic number-theoretic interface before Möbius or bigOmega applications are layered on. No link to the Recognition forcing chain or phi-ladder appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.