OAI/Combinatorics/KMedian/Binary/BinaryRationalFold.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.Binary.HasHeight.foldAdd line 14
  2. theorem OAI.MetricKMedian.Binary.HasHeight.foldMul line 22
  3. theorem OAI.MetricKMedian.Binary.ListAlgorithms.foldAdd line 32
  4. theorem OAI.MetricKMedian.Binary.ListAlgorithms.foldMul line 36
  5. def OAI.MetricKMedian.Binary.PolyProgram.ratFoldAdd line 42
  6. def OAI.MetricKMedian.Binary.PolyProgram.ratFoldMul line 50
  7. def OAI.MetricKMedian.Binary.PolyProgram.ratSum line 58
  8. def OAI.MetricKMedian.Binary.PolyProgram.ratProd line 63