OAI/Combinatorics/KMedian/Binary/BinaryRational.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Binary.Ratio.parts line 14
  2. def OAI.MetricKMedian.Binary.Ratio.encode line 15
  3. def OAI.MetricKMedian.Binary.Ratio.normalized line 16
  4. theorem OAI.MetricKMedian.Binary.Ratio.normalized_eq line 19
  5. theorem OAI.MetricKMedian.Binary.Ratio.inv_eq line 25
  6. def OAI.MetricKMedian.Binary.PolyProgram.intLT line 44
  7. def OAI.MetricKMedian.Binary.PolyProgram.intEQ line 46
  8. def OAI.MetricKMedian.Binary.PolyProgram.mkRational line 49
  9. def OAI.MetricKMedian.Binary.PolyProgram.ratNum line 65
  10. def OAI.MetricKMedian.Binary.PolyProgram.ratDen line 67
  11. def OAI.MetricKMedian.Binary.PolyProgram.ratNeg line 69
  12. def OAI.MetricKMedian.Binary.PolyProgram.ratOfInt line 73
  13. def OAI.MetricKMedian.Binary.PolyProgram.ratOfNat line 75
  14. def OAI.MetricKMedian.Binary.PolyProgram.ratMul line 77
  15. def OAI.MetricKMedian.Binary.PolyProgram.ratAdd line 83
  16. def OAI.MetricKMedian.Binary.PolyProgram.ratSub line 91
  17. def OAI.MetricKMedian.Binary.PolyProgram.ratInv line 93
  18. def OAI.MetricKMedian.Binary.PolyProgram.ratDiv line 95
  19. def OAI.MetricKMedian.Binary.PolyProgram.ratLT line 97