prime_onehundredfiftyone
plain-language theorem explainer
The declaration establishes that 151 is a prime natural number. Researchers working on arithmetic functions or Möbius inversion would cite this for concrete small-prime instances in calculations. The proof applies a native decision procedure that evaluates primality by direct computation.
Claim. The natural number $151$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local theoretical setting keeps statements minimal so that Dirichlet inversion can be added once interfaces stabilize. The sole upstream dependency is the alias Prime, defined as the standard Nat.Prime predicate on natural numbers.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the primality predicate computationally.
why it matters
This supplies a basic concrete prime inside the arithmetic-functions module. It can support later Möbius evaluations on squarefree or prime-power inputs, though no downstream uses are recorded. The result sits outside the Recognition Science forcing chain and does not reference phi, the eight-tick octave, or constants such as G or alpha.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.