mod4_eightythree_prime
plain-language theorem explainer
83 is a prime congruent to 3 modulo 4. Number theorists examining residue classes or preparing inputs for arithmetic functions such as the Möbius function would cite this explicit example. The proof reduces to a single native decision procedure that verifies both primality and the congruence in one step.
Claim. $83$ is prime and $83 ≡ 3 mod 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard predicate that a natural number has no divisors other than 1 and itself. The local setting consists of basic facts about specific primes that can later support Dirichlet inversion or squarefree checks.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of primality and the modular condition.
why it matters
The declaration supplies a concrete prime in the residue class 3 mod 4 that can serve as a test case for arithmetic-function identities in the module. It fills a basic number-theoretic slot without direct reference to the forcing chain or phi-ladder, and no downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.