sophie_germain_two
plain-language theorem explainer
The declaration asserts that 2 is a Sophie Germain prime by confirming both 2 and 5 are prime. Number theorists referencing base cases for safeprime pairs or arithmetic-function applications would cite this instance. The proof reduces the claim to a direct computational check via native_decide.
Claim. $2$ is prime and $5$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the local alias for the standard primality predicate on natural numbers. The theorem records a concrete Sophie Germain pair as a verified base fact in the primes section.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the primality of 2 and 5.
why it matters
This supplies a verified base case for Sophie Germain primes inside the number-theory layer. It supports downstream arithmetic-function work even though no immediate uses are recorded. The fact aligns with the need for explicit small-prime instances when building Möbius-based identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.