safe_prime_seven
plain-language theorem explainer
The declaration verifies that 7 is a safe prime by confirming primality of both 7 and 3. Number theorists building examples with arithmetic functions or small primes would cite this for concrete base cases. The proof reduces the entire statement to a single native_decide computation that discharges the decidable predicate.
Claim. $7$ is prime and $3$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related squarefree checks. Prime is the local transparent alias for the standard predicate on natural numbers. This theorem appears among sibling facts on Möbius values at primes and squarefree integers.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the two primality statements.
why it matters
The result supplies a verified small safe prime inside the arithmetic functions module. It anchors basic prime facts that later Möbius and big-Omega constructions can reference, though no downstream uses are recorded yet. It fits the framework's pattern of explicit small-integer checks that precede phi-ladder and mass-formula steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.