`primeCounting`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 349 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 349.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

 346/-! ### Prime counting function π -/
 347
 348/-- The prime counting function π(n) = #{p ≤ n : p prime}. -/
 349def primeCounting (n : ℕ) : ℕ := Nat.primeCounting n
 350
 351@[simp] theorem primeCounting_def {n : ℕ} : primeCounting n = Nat.primeCounting n := rfl
 352
 353/-- π(0) = 0. -/
 354theorem primeCounting_zero : primeCounting 0 = 0 := by
 355  simp [primeCounting]
 356
 357/-- π(1) = 0. -/
 358theorem primeCounting_one : primeCounting 1 = 0 := by
 359  simp [primeCounting, Nat.primeCounting]
 360
 361/-- π(2) = 1. -/
 362theorem primeCounting_two : primeCounting 2 = 1 := by
 363  native_decide
 364
 365/-- π(3) = 2. -/
 366theorem primeCounting_three : primeCounting 3 = 2 := by
 367  native_decide
 368
 369/-- π(5) = 3. -/
 370theorem primeCounting_five : primeCounting 5 = 3 := by
 371  native_decide
 372
 373/-- π(10) = 4. -/
 374theorem primeCounting_ten : primeCounting 10 = 4 := by
 375  native_decide
 376
 377/-- π(7) = 4. -/
 378theorem primeCounting_seven : primeCounting 7 = 4 := by
 379  native_decide

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.