prime_seventynine
plain-language theorem explainer
79 is established as a prime natural number. Number theorists constructing explicit lists of small primes for arithmetic function calculations would reference this result. The verification proceeds via an automated decision procedure that confirms the property for this fixed integer.
Claim. $79$ is prime, where primality is the standard predicate on natural numbers.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. Statements remain basic here, with deeper Dirichlet algebra deferred until interfaces stabilize. The upstream definition aliases the standard primality predicate on natural numbers.
proof idea
A one-line wrapper applies the decide tactic to confirm primality for the fixed integer 79.
why it matters
The declaration supplies a verified small prime instance usable in arithmetic function definitions such as those involving the Möbius function. It stands apart from Recognition Science landmarks including the forcing chain from T0 to T8, the J-uniqueness relation, and the phi-ladder, serving only as a number-theoretic building block with no downstream citations in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.