OAI/NumberTheory/ShortEgyptian/ListConstruction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShortEgyptian.deterministicProduct line 12
  2. lemma OAI.ShortEgyptian.deterministicProduct_pos line 15
  3. lemma OAI.ShortEgyptian.deterministicProduct_injective line 21
  4. def OAI.ShortEgyptian.auxiliaryDenominator line 41
  5. lemma OAI.ShortEgyptian.auxiliaryDenominator_pos line 45
  6. lemma OAI.ShortEgyptian.two_pow_dvd_auxiliary line 53
  7. lemma OAI.ShortEgyptian.deterministic_dvd_auxiliary line 58
  8. lemma OAI.ShortEgyptian.sample_dvd_auxiliary line 67
  9. lemma OAI.ShortEgyptian.products_scale_bound line 82
  10. lemma OAI.ShortEgyptian.deterministicProduct_bound line 100
  11. lemma OAI.ShortEgyptian.sampleProduct_pos line 113
  12. lemma OAI.ShortEgyptian.sampleProduct_bound line 117