mod4_seventyone_prime
plain-language theorem explainer
71 is prime and congruent to 3 modulo 4. Number theorists verifying small cases for quadratic residues or Möbius inversion over residue classes would cite this instance. The proof is a one-line wrapper that applies native_decide to evaluate primality and the modular condition by direct computation.
Claim. $71$ is prime and $71 ≡ 3 mod 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the repo-local alias for Mathlib's Nat.Prime, kept transparent as an abbrev. This supplies a concrete prime in the 3 mod 4 class for use in arithmetic function statements.
proof idea
The proof is a one-line wrapper that invokes native_decide to confirm both the primality predicate and the residue condition by direct evaluation.
why it matters
It provides an explicit verified fact about a small prime in a specific residue class inside the arithmetic functions layer. No downstream theorems are recorded, so it serves as a basic data point for potential Möbius or squarefree checks involving primes ≡ 3 mod 4.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.