mod4_fortythree_prime
plain-language theorem explainer
43 is prime and satisfies the congruence 43 ≡ 3 (mod 4). Number theorists checking residue classes for applications of quadratic reciprocity or Möbius inversion over primes would reference this specific instance. The proof reduces to a single native decision procedure that evaluates both conditions by direct computation.
Claim. $43$ is prime and $43 ≡ 3$ (mod $4$).
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime n is the transparent alias for the standard predicate that n is prime. The local setting defers deeper Dirichlet series and inversion formulas until the basic interfaces stabilize.
proof idea
One-line wrapper that applies the native_decide tactic to evaluate the conjunction of primality and the modular arithmetic condition.
why it matters
The declaration supplies a concrete modular prime fact inside the arithmetic-functions module. It supports potential later use of the Möbius function on primes in the 3 mod 4 class, consistent with the module's role as a foothold for number-theoretic primitives. No downstream applications are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.