OAI/NumberTheory/Jacobsthal/Primes/LargePrimeDeletion.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.cutoffPrimes line 19
  2. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.mem_cutoffPrimes line 22
  3. def OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.largePrimeFactors line 26
  4. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.mem_largePrimeFactors line 29
  5. def OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.deletionCell line 33
  6. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.mem_deletionCell line 37
  7. def OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.divisibilityResidue line 42
  8. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.divisibility_iff_modEq line 44
  9. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.card_deletionCell_range line 54
  10. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.card_deletionCell_le_div_add_one line 63
  11. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.card_deletionCell_le_real_div_add_one line 75
  12. def OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.cutoffSurvivors line 85
  13. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.mem_cutoffSurvivors line 89
  14. def OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.CompatibleSmallResidues line 97
  15. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.divisibilityResidues_compatible line 100
  16. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.cutoffSurvivors_avoid_small line 105
  17. def OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.coprimeOffsets line 117
  18. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.mem_coprimeOffsets line 121
  19. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.coprime_iff_avoid_primeFactors line 126
  20. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.candidate_subset_coprime_union_deletions line 139
  21. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.card_le_coprime_add_large_deletions line 161
  22. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.exists_coprime_of_survivor_budget line 178
  23. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.large_deletionCell_le_cutoff line 204
  24. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.sum_large_deletions_le_elementary line 216
  25. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.exists_coprime_of_cutoff_estimates line 233
  26. theorem OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.isJacobsthalBound_of_cutoff_estimates line 251