OAI/Combinatorics/KMedianRecovery/Recovery/MulComputes.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.Signed.mul_computes line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.Signed.le_computes line 29
  3. def OAI.MetricKMedianRecovery.BitMachine.Signed.add line 48
  4. def OAI.MetricKMedianRecovery.BitMachine.Signed.mul line 53
  5. def OAI.MetricKMedianRecovery.BitMachine.Signed.le line 58
  6. def OAI.MetricKMedianRecovery.BitMachine.Signed.neg line 63
  7. def OAI.MetricKMedianRecovery.BitMachine.Signed.subtraction line 66
  8. def OAI.MetricKMedianRecovery.BitMachine.Signed.multiplication line 73
  9. def OAI.MetricKMedianRecovery.BitMachine.Signed.lessEqual line 78
  10. lemma OAI.MetricKMedianRecovery.BitMachine.Signed.natAbs_signed line 83
  11. lemma OAI.MetricKMedianRecovery.BitMachine.Signed.signed_div_nat line 85
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.encode line 93
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.numerator line 94
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.denominator line 95
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.decode line 96
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.decode_encode line 98
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.divisor line 102
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.reduceNonzero line 105
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.reduce line 110
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.numerator_computes line 113
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.denominator_computes line 114
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.divisor_computes line 115
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.reduceNonzero_computes line 119
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.reduce_computes line 126
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.reduce_correct line 132
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.normalize_computes line 153
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.normalize line 158