OAI/Combinatorics/KMedianRecovery/Encoding/DivNatWords.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.Signed.signed_ediv_nat line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.Signed.divNatWords line 24
  3. def OAI.MetricKMedianRecovery.BitMachine.Signed.divNatWords_computes line 32
  4. lemma OAI.MetricKMedianRecovery.BitMachine.Signed.divNatWords_spec line 48
  5. def OAI.MetricKMedianRecovery.BitMachine.Signed.divisionNat line 55
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.floorWords line 63
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.floorWords_computes line 64
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.floorWords_encode line 65
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.floor line 68
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.ceilWords line 71
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.ceilWords_computes line 72
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.ceilWords_encode line 74
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.ceil line 77
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.castIntWords line 80
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.castIntWords_computes line 81
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.castIntWords_encode line 82
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.castInt line 84