OAI/NumberTheory/ShortEgyptian/Basic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShortEgyptian.unitSum line 7
  2. theorem OAI.ShortEgyptian.isExpansion_iff line 10
  3. def OAI.ShortEgyptian.IsUnitSum line 19
  4. def OAI.ShortEgyptian.quotient line 22
  5. def OAI.ShortEgyptian.residue line 24
  6. theorem OAI.ShortEgyptian.quotient_spec line 26
  7. theorem OAI.ShortEgyptian.residue_spec line 41
  8. theorem OAI.ShortEgyptian.residue_identity line 48
  9. theorem OAI.ShortEgyptian.predecessor_dvd line 71
  10. theorem OAI.ShortEgyptian.unitSum_nil line 75
  11. theorem OAI.ShortEgyptian.unitSum_cons line 77
  12. theorem OAI.ShortEgyptian.unitSum_append line 80
  13. theorem OAI.ShortEgyptian.unitSum_nonneg line 84
  14. theorem OAI.ShortEgyptian.unit_le_sum line 91
  15. theorem OAI.ShortEgyptian.unitSum_scale line 99