pythagorean_prime_onehundredone
plain-language theorem explainer
101 is prime and congruent to 1 modulo 4, making it a Pythagorean prime. Number theorists working on sums of two squares or classification of primes in arithmetic progressions would cite this concrete case. The verification is a direct computational check performed by the native_decide tactic.
Claim. The integer 101 is prime and satisfies $101 ≡ 1 mod 4$.
background
The ArithmeticFunctions module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The local setting keeps statements basic before any deeper Dirichlet algebra is added. The Prime predicate is the repo-local alias for the standard natural-number primality condition.
proof idea
The proof is a one-line term that applies native_decide to evaluate the conjunction of primality and the modular condition by direct computation.
why it matters
This supplies a verified Pythagorean prime instance inside the number theory primitives of the module. It populates basic facts without recorded parent theorems or downstream applications. No connection to the forcing chain or J-uniqueness is made here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.