prime_onehundredtwentyseven
plain-language theorem explainer
127 satisfies the definition of primality in the natural numbers. Number theorists working with arithmetic functions such as the Möbius function would cite this fact when handling small primes in explicit calculations. The verification proceeds by direct computational evaluation of the primality predicate.
Claim. The natural number 127 is prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function and related objects such as big-Omega. The local setting keeps statements minimal to allow later layering of Dirichlet algebra and inversion formulas. The sole upstream dependency defines Prime as the standard primality predicate on natural numbers.
proof idea
The proof applies the native_decide tactic, which evaluates the primality condition by direct computation.
why it matters
This supplies a verified primality fact inside the arithmetic functions module. It supports basic checks needed for Möbius properties and squarefree-related lemmas without invoking deeper algebraic structure. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.