OAI/NumberTheory/ShortEgyptian/GreedyPreparation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ShortEgyptian.greedy_step line 9
  2. def OAI.ShortEgyptian.Prepared line 57
  3. lemma OAI.ShortEgyptian.prepared_of_large line 62
  4. lemma OAI.ShortEgyptian.prepared_zero line 66
  5. lemma OAI.ShortEgyptian.prepared_cons line 69
  6. lemma OAI.ShortEgyptian.prepare_aux line 85
  7. lemma OAI.ShortEgyptian.prepare_denominator line 130
  8. def OAI.ShortEgyptian.greedySteps line 151
  9. def OAI.ShortEgyptian.greedyConstant line 154
  10. lemma OAI.ShortEgyptian.greedyConstant_pos line 156
  11. lemma OAI.ShortEgyptian.greedy_power_cap line 162
  12. lemma OAI.ShortEgyptian.greedy_length_bound line 173