mod4_seventynine_prime
plain-language theorem explainer
79 is a prime congruent to 3 modulo 4. Researchers working with the Möbius function or explicit small primes in residue class computations would cite this fact for concrete checks. The proof is a one-line native_decide evaluation of the conjunction.
Claim. 79 is prime and $79 ≡ 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 Nat.Prime. This supplies a concrete prime instance satisfying a modular condition, available for squarefree or arithmetic function evaluations.
proof idea
One-line wrapper that applies native_decide to evaluate the conjunction of the primality predicate and the remainder condition.
why it matters
This supplies an explicit prime fact inside the arithmetic functions module. It supports potential Möbius applications over primes in the 3 mod 4 class, though no downstream theorems currently depend on it. It provides a basic constant for number-theoretic checks within the Recognition Science number theory layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.