primeCounting_onehundredfifty
plain-language theorem explainer
The declaration asserts that the prime counting function evaluates to 35 at 150. Number theorists checking explicit values or building tables for prime distribution would reference this evaluation. The proof is a one-line native decision that computes the count directly from the definition.
Claim. $π(150) = 35$, where $π(n)$ counts the primes $p ≤ n$.
background
The prime counting function is defined by π(n) = #{p ≤ n : p prime} and implemented as a direct wrapper around Mathlib's Nat.primeCounting. The module supplies lightweight interfaces for arithmetic functions, beginning with the Möbius function μ, before layering Dirichlet algebra. The local setting keeps statements minimal to stabilize basic definitions.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the equality from the primeCounting definition.
why it matters
This supplies an explicit numerical anchor for the prime counting function inside the arithmetic functions module. It supports verification steps in prime distribution work, though no downstream theorems depend on it yet. In the Recognition framework it provides a concrete check point on the prime ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.