prime_seventyone
plain-language theorem explainer
71 is a prime natural number. Number theorists using arithmetic functions such as the Möbius function in small-case verifications would reference this fact. The proof is a direct computational check via the decide tactic on the underlying primality predicate.
Claim. $71$ is a prime natural number, where primality means the predicate that holds precisely when a natural number has no divisors other than 1 and itself.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function and keeping statements simple before deeper Dirichlet algebra is added. The local setting treats basic number-theoretic predicates as transparent interfaces. The upstream result defines the primality predicate as the direct alias for the standard natural-number primality condition.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify the primality predicate computationally.
why it matters
This supplies a concrete primality fact inside the arithmetic-functions module, supporting any later Möbius or inversion steps that require small primes. It sits among the basic number-theoretic footholds that the Recognition framework assembles before linking to forcing-chain or phi-ladder constructions, though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.