pythagorean_prime_onehundrednine
plain-language theorem explainer
109 qualifies as a Pythagorean prime by being both prime and congruent to 1 modulo 4. Number theorists examining primes that decompose into sums of two squares reference such specific cases. The verification executes as a direct native computation without manual lemmas.
Claim. $109$ is a prime number and $109 ≡ 1 mod 4$.
background
This module supplies small wrappers around Mathlib's arithmetic function library, with initial focus on the Möbius function. The declaration asserts a basic arithmetic property of the integer 109. It rests on the transparent abbreviation Prime n := Nat.Prime n from the Basic primes module.
proof idea
A one-line term proof invokes native_decide to evaluate the conjunction of primality and the modular arithmetic condition.
why it matters
The result supplies a concrete Pythagorean prime instance in the NumberTheory.Primes section. It supports enumeration tasks within arithmetic functions but shows no recorded downstream citations. The fact aligns with standard number theory but does not engage the Recognition Science forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.