prime_twentythree
plain-language theorem explainer
23 is established as a prime number in the naturals. Number theorists assembling small-prime base cases for arithmetic functions would cite it when initializing Möbius or divisor calculations. The proof is a direct decision procedure that verifies the property by exhaustive computation.
Claim. The natural number 23 is prime, i.e., its only positive divisors are 1 and itself.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for Nat.Prime. The declaration sits in a section of additional small-prime facts that support later divisor and square-free checks.
proof idea
One-line wrapper that applies the decide tactic to the decidable predicate Prime 23.
why it matters
Supplies a concrete prime instance inside the arithmetic-functions module. It prepares base cases for Möbius properties on primes but carries no direct link to the forcing chain, phi-ladder, or Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.