theorem
proved
primeCounting_zero
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 354.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
380
381/-- π(11) = 5. -/
382theorem primeCounting_eleven : primeCounting 11 = 5 := by
383 native_decide
384