OAI/NumberTheory/Jacobsthal/Sieve/AlignedCofactorSplit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosVarianceEffective.alignedPrimeFactors line 15
  2. def OAI.Erdos970.ErdosVarianceEffective.alignedPrimeProduct line 18
  3. def OAI.Erdos970.ErdosVarianceEffective.alignedCofactor line 21
  4. theorem OAI.Erdos970.ErdosVarianceEffective.badPrimeProduct_pos line 24
  5. theorem OAI.Erdos970.ErdosVarianceEffective.alignedPrimeProduct_pos line 27
  6. theorem OAI.Erdos970.ErdosVarianceEffective.aligned_bad_product line 30
  7. theorem OAI.Erdos970.ErdosVarianceEffective.alignedCofactor_eq_product line 35
  8. theorem OAI.Erdos970.ErdosVarianceEffective.alignedCofactor_pos line 41
  9. theorem OAI.Erdos970.ErdosVarianceEffective.alignedCofactor_mul_bad line 46
  10. theorem OAI.Erdos970.ErdosVarianceEffective.alignedCofactor_coprime_den line 51
  11. theorem OAI.Erdos970.ErdosVarianceEffective.alignedCofactor_coprime_bad line 60