Documentation Verification Report

eSHP

📁 Source: PrimeNumberTheoremAnd/eSHP.lean

Statistics

MetricCount
Definitions0
Theoremsexists_prime_gap, exists_prime_gap_record_le, first_gap_1, first_gap_2, first_gap_3, first_gap_4, first_gap_5, first_gap_6, first_gap_7, first_gap_odd_gt_1, max_prime_gap, nth_prime_vals, table_8_prime_gap, table_8_prime_gap_complete, table_8_prime_gap_complete_test, table_8_prime_gap_test, table_9_prime_gap, table_9_prime_gap_complete, table_9_prime_gap_complete_test, table_9_prime_gap_test
20
Total20
⚠️ With sorryexists_prime_gap, table_8_prime_gap, table_8_prime_gap_complete, table_9_prime_gap, table_9_prime_gap_complete
5

eSHP

Theorems

NameKindAssumesProvesValidatesDepends On
exists_prime_gap 📖 ⚠️mathematicalfirst_gap
exists_prime_gap_record_le 📖mathematicalnth_prime
nth_prime_gap
prime_gap_record
first_gap_1 📖mathematicalfirst_gapnth_prime_vals
first_gap_2 📖mathematicalfirst_gapnth_prime_vals
first_gap_3 📖mathematicalfirst_gapfirst_gap_odd_gt_1
first_gap_4 📖mathematicalfirst_gap
first_gap_5 📖mathematicalfirst_gapfirst_gap_odd_gt_1
first_gap_6 📖mathematicalfirst_gapnth_prime_vals
first_gap_7 📖mathematicalfirst_gapfirst_gap_odd_gt_1
first_gap_odd_gt_1 📖mathematicalfirst_gap
max_prime_gap 📖mathematicalnth_primenth_prime_gapexists_prime_gap_record_le
table_8_prime_gap_complete
nth_prime_vals 📖mathematicalnth_prime
table_8_prime_gap 📖 ⚠️mathematicaltable_8prime_gap_record
table_8_prime_gap_complete 📖 ⚠️mathematicalprime_gap_recordtable_8
table_8_prime_gap_complete_test 📖mathematicalprime_gap_recordtable_8
table_8_prime_gap_test 📖mathematicaltable_8prime_gap_record
table_9_prime_gap 📖 ⚠️mathematicaltable_9first_gap_record
table_9_prime_gap_complete 📖 ⚠️mathematicalfirst_gap_recordtable_9
table_9_prime_gap_complete_test 📖mathematicalfirst_gap_recordtable_9first_gap_7
first_gap_6
first_gap_5
first_gap_4
first_gap_3
first_gap_2
first_gap_1
table_9_prime_gap_test 📖mathematicaltable_9first_gap_record

---

← Back to Index