primeCounting_ten
plain-language theorem explainer
The declaration establishes that the prime counting function evaluates to 4 at input 10. Number theorists checking small explicit cases of arithmetic functions would cite this result. The proof reduces the equality to a single native decision procedure that computes the count directly.
Claim. $π(10) = 4$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The prime counting function is introduced as π(n) = #{p ≤ n : p prime}, with its definition delegating to the underlying Nat.primeCounting implementation. The local setting keeps statements minimal to permit later addition of Dirichlet algebra and inversion once the basic interfaces stabilize.
proof idea
The proof is a one-line term that applies native_decide to confirm the equality by direct evaluation.
why it matters
This supplies a concrete verification point for the prime counting definition inside the arithmetic functions module. It anchors basic counting facts before Möbius inversion or deeper Dirichlet structures are layered on, consistent with the module's stated goal of providing footholds for later work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.