pythagorean_prime_seventythree
plain-language theorem explainer
73 is a prime congruent to 1 modulo 4 and therefore a Pythagorean prime. Number theorists working on sums of two squares or prime classification would reference this concrete case. The verification is a direct computation that applies Lean's native decision procedure to the conjunction.
Claim. $73$ is prime and $73 ≡ 1 mod 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Pythagorean primes are those congruent to 1 modulo 4; by Fermat's theorem they admit a representation as a sum of two squares. The local Prime predicate is the standard Nat.Prime abbreviation.
proof idea
The proof is a one-line wrapper that invokes native_decide on the decidable proposition Prime 73 ∧ 73 % 4 = 1.
why it matters
The declaration supplies a concrete instance of a small Pythagorean prime inside the arithmetic-functions layer. It sits alongside the Möbius definitions but does not feed any recorded downstream theorems. No direct link to the forcing chain or phi-ladder appears in the surrounding material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.