mod6_twentythree_prime
plain-language theorem explainer
23 is established as prime and congruent to 5 modulo 6. Number theorists working on residue classes of small primes or modular constraints may cite this fact. The proof applies a native decision procedure to settle the concrete numerical statement directly.
Claim. $23$ is prime and $23 ≡ 5 mod 6$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. This theorem records a basic modular fact about the prime 23 within the NumberTheory.Primes hierarchy. It depends on the upstream alias Prime, defined as the standard Nat.Prime predicate.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the conjunction of primality and the modular condition.
why it matters
This fact supplies a concrete numerical anchor in the primes module. It supports modular arithmetic checks on small primes before deeper Dirichlet or inversion results are layered on. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.