mod4_seven_prime
plain-language theorem explainer
The declaration establishes that 7 is prime and 7 ≡ 3 mod 4. Number theorists handling specific cases of quadratic residues or arithmetic functions over primes congruent to 3 mod 4 would cite this instance. The proof is a one-line wrapper that applies native_decide to evaluate the conjunction directly.
Claim. $7$ is prime and $7 ≡ 3 (mod 4)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This theorem provides a basic prime fact inside that setting. The sole upstream dependency is the transparent alias Prime n := Nat.Prime n from the Basic module.
proof idea
The proof is a one-line wrapper that invokes native_decide to confirm both primality and the modular condition by direct computation.
why it matters
This supplies a concrete verified instance of a prime ≡ 3 mod 4 inside the arithmetic-functions module. It supports potential later use of the Möbius function on squarefree integers involving such primes, consistent with the file's focus on Dirichlet algebra footholds. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.