OAI/Combinatorics/EditApproximation/Binary/UnreducedRational.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Exact fractions with positive, unreduced denominators. These operations perform no greatest-common-divisor computation. The representation lemmas apply to the intermediate fractions, not merely their reduced Rat values.

  1. theorem OAI.EditApproximation.UnreducedRational.eq_of_num_den line 18
  2. def OAI.EditApproximation.UnreducedRational.ofRat line 27
  3. def OAI.EditApproximation.UnreducedRational.add line 31
  4. def OAI.EditApproximation.UnreducedRational.neg line 34
  5. def OAI.EditApproximation.UnreducedRational.le line 42
  6. def OAI.EditApproximation.UnreducedRational.storageBits line 46
  7. theorem OAI.EditApproximation.UnreducedRational.value_ofRat line 48
  8. theorem OAI.EditApproximation.UnreducedRational.value_zero line 51
  9. theorem OAI.EditApproximation.UnreducedRational.value_add line 53
  10. theorem OAI.EditApproximation.UnreducedRational.value_neg line 60
  11. theorem OAI.EditApproximation.UnreducedRational.value_mul line 63
  12. theorem OAI.EditApproximation.UnreducedRational.value_inv line 66
  13. theorem OAI.EditApproximation.UnreducedRational.value_div line 80
  14. theorem OAI.EditApproximation.UnreducedRational.le_eq_true line 83
  15. theorem OAI.EditApproximation.UnreducedRational.lt_eq_true line 89
  16. theorem OAI.EditApproximation.UnreducedRational.add_den_bits line 95
  17. theorem OAI.EditApproximation.UnreducedRational.mul_den_bits line 99
  18. theorem OAI.EditApproximation.UnreducedRational.num_abs_le line 103
  19. theorem OAI.EditApproximation.UnreducedRational.storageBits_le line 115