OAI/Combinatorics/KMedian/Binary/BinaryInteger.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Binary.Signed.value line 14
  2. def OAI.MetricKMedian.Binary.Signed.sign line 15
  3. def OAI.MetricKMedian.Binary.Signed.parts line 16
  4. def OAI.MetricKMedian.Binary.Signed.encode line 17
  5. theorem OAI.MetricKMedian.Binary.Signed.abs_value line 19
  6. theorem OAI.MetricKMedian.Binary.Signed.sign_value line 20
  7. theorem OAI.MetricKMedian.Binary.Signed.value_parts line 25
  8. theorem OAI.MetricKMedian.Binary.Signed.value_neg line 31
  9. theorem OAI.MetricKMedian.Binary.Signed.value_mul line 34
  10. def OAI.MetricKMedian.Binary.Signed.add line 37
  11. theorem OAI.MetricKMedian.Binary.Signed.value_add line 40
  12. theorem OAI.MetricKMedian.Binary.Signed.value_div line 43
  13. abbrev OAI.MetricKMedian.Binary.PolyProgram.signedParts line 49
  14. def OAI.MetricKMedian.Binary.PolyProgram.intFromParts line 51
  15. def OAI.MetricKMedian.Binary.PolyProgram.intSign line 58
  16. def OAI.MetricKMedian.Binary.PolyProgram.intAbs line 60
  17. def OAI.MetricKMedian.Binary.PolyProgram.intNeg line 63
  18. def OAI.MetricKMedian.Binary.PolyProgram.intOfNat line 67
  19. def OAI.MetricKMedian.Binary.PolyProgram.boolXor line 70
  20. def OAI.MetricKMedian.Binary.PolyProgram.boolEq line 72
  21. def OAI.MetricKMedian.Binary.PolyProgram.intMul line 75
  22. def OAI.MetricKMedian.Binary.PolyProgram.intAdd line 83
  23. def OAI.MetricKMedian.Binary.PolyProgram.intSub line 99