prime_eightythree
plain-language theorem explainer
The declaration asserts that 83 satisfies the standard definition of primality in the naturals. Number theorists using the module's arithmetic-function wrappers would cite it when confirming small primes for Möbius calculations. The proof is a direct computational check via the decide tactic.
Claim. $83$ is a prime natural number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the repo-local alias for the standard Nat.Prime predicate. The local setting keeps statements minimal to support later Dirichlet inversion once interfaces stabilize.
proof idea
One-line wrapper that applies the decide tactic to verify the primality definition for 83.
why it matters
The result supplies a basic primality fact inside the arithmetic-functions module. It supports sibling statements on the Möbius function and square-freeness. No downstream uses are recorded, so it functions as isolated infrastructure rather than a chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.