OAI/Combinatorics/KMedianRecovery/Encoding/Words.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.RatOps.ofWords line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.RatOps.nat line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.RatOps.const line 18
  4. def OAI.MetricKMedianRecovery.BitMachine.RatOps.add line 19
  5. def OAI.MetricKMedianRecovery.BitMachine.RatOps.mul line 24
  6. def OAI.MetricKMedianRecovery.BitMachine.RatOps.sub line 29
  7. def OAI.MetricKMedianRecovery.BitMachine.RatOps.div line 34
  8. def OAI.MetricKMedianRecovery.BitMachine.RatOps.inv line 39
  9. def OAI.MetricKMedianRecovery.BitMachine.RatOps.neg line 43
  10. def OAI.MetricKMedianRecovery.BitMachine.RatOps.floor line 47
  11. def OAI.MetricKMedianRecovery.BitMachine.RatOps.root line 54