theorem
proved
primeCounting_seven
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 378.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
375 native_decide
376
377/-- π(7) = 4. -/
378theorem primeCounting_seven : primeCounting 7 = 4 := by
379 native_decide
380
381/-- π(11) = 5. -/
382theorem primeCounting_eleven : primeCounting 11 = 5 := by
383 native_decide
384
385/-- π(13) = 6. -/
386theorem primeCounting_thirteen : primeCounting 13 = 6 := by
387 native_decide
388
389/-- π(17) = 7. -/
390theorem primeCounting_seventeen : primeCounting 17 = 7 := by
391 native_decide
392
393/-- π(20) = 8. -/
394theorem primeCounting_twenty : primeCounting 20 = 8 := by
395 native_decide
396
397/-- π(100) = 25. -/
398theorem primeCounting_hundred : primeCounting 100 = 25 := by
399 native_decide
400
401/-- π is monotone: m ≤ n → π(m) ≤ π(n). -/
402theorem primeCounting_mono {m n : ℕ} (h : m ≤ n) : primeCounting m ≤ primeCounting n := by
403 simp only [primeCounting]
404 exact Nat.monotone_primeCounting h
405
406/-! ### Liouville-squarefree connection -/
407
408/-- For squarefree n, λ(n) = μ(n). -/