pythagorean_prime_seventeen
plain-language theorem explainer
17 is prime and congruent to 1 modulo 4, confirming it as a Pythagorean prime. Number theorists working on sums of two squares or quadratic forms would cite this concrete case. The proof is a direct computational verification with no intermediate lemmas.
Claim. $17$ is prime and $17$ satisfies $17$ ≡ 1 (mod 4).
background
The module supplies lightweight wrappers around arithmetic functions, starting with the Möbius function μ. Primality is the standard predicate on natural numbers. The declaration depends on the basic primality definition imported from the primes module and on computational decision procedures.
proof idea
This is a one-line wrapper that applies native_decide to evaluate the conjunction of primality and the residue condition.
why it matters
It records a specific Pythagorean prime inside the arithmetic functions module. The fact can support later Möbius inversion statements over primes congruent to 1 mod 4. No downstream uses appear in the current dependency graph and no direct tie to the forcing chain or Recognition constants is present.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.