mod4_fortyseven_prime
plain-language theorem explainer
47 is prime and congruent to 3 modulo 4. Researchers verifying explicit cases in quadratic reciprocity or Dirichlet characters modulo 4 would cite the fact for small checks. The proof is a one-line wrapper that applies native_decide to evaluate the conjunction directly.
Claim. $47$ is prime and $47$ satisfies $47 ≡ 3 mod 4$.
background
The module supplies lightweight wrappers around arithmetic functions, beginning with the Möbius function μ. The local setting keeps statements basic to allow later layering of Dirichlet algebra and inversion. The sole upstream dependency is the alias Prime n, defined as the standard primality predicate on natural numbers and kept transparent.
proof idea
The proof is a one-line wrapper that invokes native_decide to resolve both the primality predicate and the modulo condition by direct computation.
why it matters
The declaration supplies an explicit prime in the 3 mod 4 class for arithmetic function work in the module. No downstream uses are recorded. It aligns with the need for concrete prime checks inside the number-theoretic foundations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.