OAI/NumberTheory/ShortEgyptian/ReciprocalDifferences.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShortEgyptian.reciprocalProduct line 10
  2. theorem OAI.ShortEgyptian.reciprocalProduct_nil line 13
  3. theorem OAI.ShortEgyptian.reciprocalProduct_cons line 14
  4. theorem OAI.ShortEgyptian.reciprocalProduct_shift line 17
  5. def OAI.ShortEgyptian.expandDifference line 25
  6. theorem OAI.ShortEgyptian.expandDifference_length line 30
  7. theorem OAI.ShortEgyptian.expandDifference_shape line 36
  8. theorem OAI.ShortEgyptian.reciprocalProduct_difference line 63
  9. def OAI.ShortEgyptian.backwardDifferences line 84
  10. def OAI.ShortEgyptian.reciprocalTerms line 88
  11. theorem OAI.ShortEgyptian.reciprocalTerms_shape line 92
  12. theorem OAI.ShortEgyptian.reciprocalTerms_difference line 120
  13. theorem OAI.ShortEgyptian.backwardDifferences_reciprocal line 133
  14. theorem OAI.ShortEgyptian.reciprocalProduct_bounds line 149
  15. theorem OAI.ShortEgyptian.backwardDifferences_reciprocal_bounds line 168