pythagorean_prime_thirteen
plain-language theorem explainer
13 qualifies as a Pythagorean prime by satisfying both primality and the congruence condition modulo 4. Number theorists examining sums of two squares or quadratic residues would reference this specific case. The proof consists of a direct computational verification using the native decision procedure.
Claim. $13$ is prime and $13 ≡ 1 (mod 4)$.
background
Prime is the repository-local transparent alias for the standard Nat.Prime predicate on natural numbers. The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ, and keeps statements minimal pending deeper Dirichlet algebra. This declaration appears among siblings handling squarefree numbers and big-Omega functions.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the conjunction of primality and the modular condition.
why it matters
This supplies a concrete Pythagorean prime instance inside the NumberTheory.Primes section. It supports arithmetic-function applications such as Möbius on squarefree inputs, though no downstream uses are recorded. The fact aligns with the framework's pattern of explicit small-case verifications that feed the phi-ladder and mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.