OAI/Combinatorics/KMedian/Compression/RationalOperationHeight.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Binary.HasHeight line 12
  2. theorem OAI.MetricKMedian.Binary.HasHeight.mono line 17
  3. theorem OAI.MetricKMedian.Binary.HasHeight.zero line 20
  4. theorem OAI.MetricKMedian.Binary.HasHeight.one line 26
  5. theorem OAI.MetricKMedian.Binary.HasHeight.neg line 30
  6. theorem OAI.MetricKMedian.Binary.HasHeight.mul line 33
  7. theorem OAI.MetricKMedian.Binary.HasHeight.inv line 47
  8. theorem OAI.MetricKMedian.Binary.HasHeight.div line 62
  9. theorem OAI.MetricKMedian.Binary.HasHeight.add line 65
  10. theorem OAI.MetricKMedian.Binary.HasHeight.sub line 91
  11. theorem OAI.MetricKMedian.Binary.HasHeight.sum line 94
  12. theorem OAI.MetricKMedian.Binary.HasHeight.partialSum line 106