prime_onehundredseventythree
plain-language theorem explainer
173 is shown to be prime via direct computation. Number theorists using the arithmetic functions library would cite this when working with the specific value 173 in Möbius calculations. The proof consists of a native_decide tactic call.
Claim. $173$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function. Prime is defined as an alias for the standard natural number primality predicate. This theorem sits among other results on Möbius and big-Omega functions for squarefree numbers.
proof idea
A one-line wrapper applies the native_decide tactic to evaluate the primality predicate computationally.
why it matters
It supplies a verified primality fact in the primes arithmetic functions module. No parent theorems are listed in the used_by edges, indicating it may serve as a foundational check for future work on arithmetic functions. It aligns with the number theory scaffolding in Recognition Science without touching the core forcing chain or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.