pythagorean_prime_fortyone
plain-language theorem explainer
41 is a prime congruent to 1 modulo 4 and therefore a Pythagorean prime. Number theorists working on sums of two squares or quadratic forms cite this as a small verified instance. The proof is a one-line computational check that evaluates both conjuncts directly.
Claim. The integer 41 is prime and satisfies $41 ≡ 1 mod 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard primality predicate on natural numbers. The local setting keeps statements minimal so that deeper Dirichlet inversion can be added once interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to confirm the conjunction by direct evaluation.
why it matters
The declaration supplies a concrete example of a 4k+1 prime inside the arithmetic-functions layer. No downstream uses are recorded. It touches the classification of primes relevant to quadratic forms but does not link directly to the core Recognition Science forcing chain or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.