theorem
proved
primeCounting_fivehundred
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 896.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
893theorem primeCounting_twohundredfifty : primeCounting 250 = 53 := by native_decide
894
895/-- π(500) = 95. -/
896theorem primeCounting_fivehundred : primeCounting 500 = 95 := by native_decide
897
898/-- π(750) = 132. -/
899theorem primeCounting_sevenhundredfifty : primeCounting 750 = 132 := by native_decide
900
901/-! ### Legendre formula concrete values -/
902
903/-- vp 2 (10!) = 8. -/
904theorem vp_factorial_ten_two : vp 2 (Nat.factorial 10) = 8 := by native_decide
905
906/-- vp 2 (12!) = 10. -/
907theorem vp_factorial_twelve_two : vp 2 (Nat.factorial 12) = 10 := by native_decide
908
909/-- vp 3 (10!) = 4. -/
910theorem vp_factorial_ten_three : vp 3 (Nat.factorial 10) = 4 := by native_decide
911
912/-- vp 3 (12!) = 5. -/
913theorem vp_factorial_twelve_three : vp 3 (Nat.factorial 12) = 5 := by native_decide
914
915/-- vp 5 (25!) = 6. -/
916theorem vp_factorial_twentyfive_five : vp 5 (Nat.factorial 25) = 6 := by native_decide
917
918/-- vp 7 (50!) = 8. -/
919theorem vp_factorial_fifty_seven : vp 7 (Nat.factorial 50) = 8 := by native_decide
920
921/-! ### More squarefree concrete values -/
922
923/-- 30 is squarefree. -/
924theorem squarefree_thirty : Squarefree 30 := by native_decide
925
926/-- 6 is squarefree. -/