safe_prime_eightythree
plain-language theorem explainer
83 qualifies as a safe prime because both 83 and 41 are prime. Number theorists maintaining arithmetic-function libraries or verifying prime lists for Recognition Science applications would cite this fact. The proof is a direct native decision that evaluates the two primality statements without case analysis or external lemmas.
Claim. $83$ is a safe prime: $83$ is prime and $(83-1)/2=41$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the repository-local transparent alias for the standard natural-number primality predicate. The theorem appears among basic prime checks that stabilize the interface before Dirichlet inversion or squarefree applications are layered on.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate both primality assertions by direct computation.
why it matters
The declaration supplies a verified safe-prime instance inside the arithmetic-functions module. It supports later Möbius-function identities that rely on prime and squarefree facts. No downstream use is recorded yet; the fact aligns with the module goal of keeping basic statements lightweight before deeper algebra is added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.