mod4_twentythree_prime
plain-language theorem explainer
23 is established as prime with residue 3 modulo 4. Number theorists checking small cases for quadratic residues or Dirichlet L-functions reference this concrete instance. The verification proceeds by direct computational decision on the conjunction of primality and the modular condition.
Claim. $23$ is prime and $23 ≡ 3 mod 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This supplies a concrete prime fact that can be invoked when evaluating arithmetic functions at small arguments. Upstream, Prime is the transparent alias for the standard Nat.Prime predicate on natural numbers.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the conjunction of primality and the modular residue by direct computation.
why it matters
This supplies a verified base case of a prime congruent to 3 mod 4 inside the arithmetic-functions module. It supports potential downstream calculations involving Möbius values or squarefree detection at 23, though no uses are recorded yet. The fact aligns with the module's role of providing small, stable footholds before deeper Dirichlet algebra is layered on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.