mod4_three_prime
plain-language theorem explainer
Number theorists classifying primes by residue classes modulo 4 cite the fact that 3 is prime and satisfies 3 ≡ 3 (mod 4). The statement supplies an elementary building block for work on arithmetic progressions and quadratic residues. The proof reduces to a single native_decide tactic that evaluates the primality predicate and modular condition by direct computation.
Claim. The integer 3 is prime and satisfies $3 ≡ 3 (mod 4)$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function μ. This theorem sits among prime-related facts that support later Dirichlet inversion steps. It depends on the upstream alias Prime (n : ℕ) : Prop := Nat.Prime n, described as the repo-local transparent alias for Mathlib’s Nat.Prime.
proof idea
The proof is a one-line term-mode wrapper that invokes the native_decide tactic to decide the conjunction of the primality predicate and the modular equality.
why it matters
The declaration records a basic prime fact inside the arithmetic-functions module. No downstream theorems are listed among the used_by edges, so it currently functions as a self-contained reference point rather than a direct input to a parent result. It aligns with the module's focus on Möbius footholds but does not yet connect to Recognition Science landmarks such as the phi-ladder or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.