mod6_fiftynine_prime
plain-language theorem explainer
59 is prime and satisfies 59 ≡ 5 (mod 6). Number theorists using arithmetic functions such as the Möbius function for small-case verifications would cite this fact when confirming prime inputs modulo 6. The proof is a one-line wrapper that applies native_decide directly to the conjunction of primality and the modular equality.
Claim. $59$ is prime and $59 ≡ 5 (mod 6)$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Prime is a transparent alias for Nat.Prime, allowing direct use in primality statements without additional hypotheses. This theorem records an explicit small prime satisfying the residue condition modulo 6, consistent with the module's focus on basic interfaces before deeper Dirichlet algebra.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction Prime 59 ∧ 59 % 6 = 5.
why it matters
This supplies a verified small-case fact for arithmetic functions involving primes. It supports downstream checks in Möbius-related properties within the NumberTheory.Primes layer, though no direct used_by links appear. It aligns with the need for explicit prime verifications before layering inversion formulas or squarefree conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.