Commit 2023-06-18 08:20 1ab29aec

View on Github →

feat: port Archive.Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges (#5208)

Estimated changes

Modified Archive.lean

Created Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

added def Theorems100.P

added theorem Theorems100.Real.tendsto_sum_one_div_prime_atTop

added def Theorems100.U

added theorem Theorems100.card_le_mul_sum

added theorem Theorems100.card_le_two_pow

added theorem Theorems100.card_le_two_pow_mul_sqrt

added theorem Theorems100.range_sdiff_eq_biUnion

added theorem Theorems100.sum_lt_half_of_not_tendsto