prime_onehundredninetyseven
plain-language theorem explainer
The theorem asserts that 197 is prime. Number theorists using arithmetic functions on small primes would cite this fact when verifying inputs for Möbius or related computations. The proof is a direct native_decide tactic that reduces the claim to an immediate computational check.
Claim. $197$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. Prime is the repo-local alias for Nat.Prime. The local setting keeps statements minimal so that deeper Dirichlet algebra can be added later once basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to perform a direct computational verification of primality.
why it matters
This supplies a concrete primality fact needed for arithmetic-function calculations on small primes. No downstream uses are recorded yet, so it functions as a basic building block rather than a link in a larger chain. It supports the module's goal of providing stable interfaces before layering inversion formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.