OAI/Combinatorics/Progressions/Lattices/LargestBadPrimeProduct.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.selected_primePower_factorization line 11
  2. theorem OAI.Erdos3.selected_primePower_primeFactors line 24
  3. theorem OAI.Erdos3.selected_primePower_factorization_of_mem line 35
  4. def OAI.Erdos3.badPrimeModulusEvent line 40
  5. theorem OAI.Erdos3.selected_primePower_badPrimeModulusEvent line 46
  6. def OAI.Erdos3.largestTestedBadDepth line 71
  7. theorem OAI.Erdos3.largestTestedBadDepth_le line 75
  8. theorem OAI.Erdos3.largestTestedBadDepth_bad line 80
  9. def OAI.Erdos3.smallPrimePowerCorrection line 90
  10. theorem OAI.Erdos3.prime_power_small_correction line 93
  11. theorem OAI.Erdos3.largestBadPrime_large_valid line 134
  12. theorem OAI.Erdos3.largestBadPrime_subproduct_modulus_event line 147