prime_thirtyone
plain-language theorem explainer
The declaration asserts that 31 satisfies the standard primality predicate on the natural numbers. Number theorists referencing arithmetic functions in this module would cite the fact when checking small prime inputs for Möbius calculations. The proof is a one-line wrapper that invokes the decide tactic to verify the predicate computationally.
Claim. The natural number $31$ is prime: it exceeds 1 and admits no positive divisors other than 1 and itself.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local setting keeps statements minimal so that deeper Dirichlet inversion can be added once basic interfaces stabilize. The sole upstream result is the transparent alias Prime n := Nat.Prime n, the standard predicate that n > 1 has no divisors other than 1 and n.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the primality predicate for 31.
why it matters
The fact supplies a concrete small-prime instance inside the NumberTheory.Primes.ArithmeticFunctions hierarchy. It supports verification steps that may later feed Möbius inversion or square-free checks, though no downstream uses are recorded. The declaration sits outside the Recognition Science forcing chain and constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.