bump

rwst · Jul 14, 2024 · 93457a3 · 93457a3
1 parent 1f6d5a0
commit 93457a3
Show file tree

Hide file tree

Showing 5 changed files with 551 additions and 144 deletions.
diff --git a/InfinitePrimesViaLog/Basic.lean b/InfinitePrimesViaLog/Basic.lean
@@ -296,3 +296,5 @@ theorem primeCountingReal_unbounded : Tendsto primeCountingReal atTop atTop := b
 
 theorem infinite_setOf_prime : { p | Nat.Prime p }.Infinite :=
   sorry
+
+end Finset
diff --git a/blueprint/lean_decls b/blueprint/lean_decls
@@ -1,20 +1,34 @@
+log_le_harmonic
+S₁
+H_P4_2
+H_P4_3
+H_P4_4a
 primeCountingReal
+H_P4_4b
+H_P4_3a
+H_P4_4
 monotone_primeCountingReal
 primeCountingReal_ge_two
 prod_Icc_succ_div
 H_P4_5
-H_P4_4a
-H_P4_4
+H_P4_1
 log_le_primeCountingReal_add_one
 primeCountingReal_unbounded
-infinity_of_primes
+infinite_setOf_prime
+log_le_harmonic
+S₁
+H_P4_2
+H_P4_3
+H_P4_4a
 primeCountingReal
+H_P4_4b
+H_P4_3a
+H_P4_4
 monotone_primeCountingReal
 primeCountingReal_ge_two
 prod_Icc_succ_div
 H_P4_5
-H_P4_4a
-H_P4_4
+H_P4_1
 log_le_primeCountingReal_add_one
 primeCountingReal_unbounded
-infinity_of_primes
+infinite_setOf_prime
Original file line number	Diff line number	Diff line change
Expand Up		@@ -296,3 +296,5 @@ theorem primeCountingReal_unbounded : Tendsto primeCountingReal atTop atTop := b

		theorem infinite_setOf_prime : { p \| Nat.Prime p }.Infinite :=
		sorry

		end Finset