OAI/Combinatorics/KMedian/Compression/IntegerListProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Binary.IntegerList.Row line 14
  2. abbrev OAI.MetricKMedian.Binary.IntegerList.Rows line 15
  3. abbrev OAI.MetricKMedian.Binary.IntegerList.er line 16
  4. abbrev OAI.MetricKMedian.Binary.IntegerList.em line 17
  5. def OAI.MetricKMedian.Binary.IntegerList.denominator line 19
  6. def OAI.MetricKMedian.Binary.IntegerList.numerators line 20
  7. theorem OAI.MetricKMedian.Binary.IntegerList.denominator_ofFn line 22
  8. theorem OAI.MetricKMedian.Binary.IntegerList.numerators_ofFn line 26
  9. def OAI.MetricKMedian.Binary.IntegerList.sumProgram line 33
  10. def OAI.MetricKMedian.Binary.IntegerList.prodProgram line 36
  11. def OAI.MetricKMedian.Binary.IntegerList.denominatorProgram line 39
  12. def OAI.MetricKMedian.Binary.IntegerList.numeratorsProgram line 41