prime_onehundredthirtynine
plain-language theorem explainer
139 is a prime natural number. Number theorists building arithmetic function interfaces in Recognition Science might cite this when verifying specific inputs for Möbius or divisor sums. The proof is a one-line computational check that exhausts possible divisors up to the square root.
Claim. The natural number $139$ satisfies the primality predicate: it has no positive divisors other than $1$ and itself.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is a transparent alias for the standard Nat.Prime predicate on natural numbers. The local setting is basic number-theoretic scaffolding for later Dirichlet inversion and squarefree checks; the only upstream dependency is the Prime alias itself.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic, reducing the primality statement to a decidable computation over the finite set of candidate divisors.
why it matters
The declaration supplies a concrete, machine-verified primality fact inside the arithmetic-functions layer. It supports downstream use of Möbius and related functions on specific integers, consistent with the need for exact number-theoretic inputs when deriving constants such as the fine-structure inverse near 137. No parent theorems or open questions are recorded in the current dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.