pythagorean_prime_ninetyseven
plain-language theorem explainer
97 is established as a prime congruent to 1 modulo 4, qualifying it as a Pythagorean prime. Number theorists enumerating primes representable as sums of two squares would reference this fact. The verification proceeds via a single native decision procedure that confirms both primality and the residue class directly.
Claim. $97$ is prime and $97$ satisfies $97 ≡ 1 mod 4$.
background
The declaration appears in the arithmetic functions module, which supplies lightweight wrappers around Mathlib's Möbius function μ and related tools for eventual Dirichlet inversion. The local setting keeps statements minimal until basic interfaces stabilize. Prime is the transparent alias for Nat.Prime supplied by the Basic submodule.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the conjunction of primality and the modular condition.
why it matters
This supplies a concrete instance of a Pythagorean prime inside the number theory layer. It supports later arithmetic function work even though no downstream uses are recorded. The result aligns with the framework's reliance on standard number-theoretic facts to anchor constants such as the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.