prime_twohundredsixtynine
plain-language theorem explainer
269 is a prime number. Number theorists building libraries of small primes for arithmetic functions such as Möbius inversion would cite this fact during factorization checks. The proof is a one-line wrapper that invokes Lean's native_decide tactic to evaluate the primality predicate by direct computation.
Claim. $269$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local setting keeps statements minimal so that deeper Dirichlet algebra and inversion can be added once basic interfaces stabilize. The Prime predicate is the repo-local alias for the standard Nat.Prime definition.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute the primality check directly.
why it matters
This theorem supplies a verified small-prime fact inside the NumberTheory.Primes module. It populates the arithmetic-function library that supports Möbius and related operations, even though no downstream use is recorded yet. The placement aligns with the module's role of providing number-theoretic footholds without invoking the forcing chain or RS constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.