OAI/Combinatorics/KMedian/Reduction/CompletionProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.Completion.Rational.Program.Input line 16
  2. abbrev OAI.MetricKMedian.Completion.Rational.Program.Raw line 24
  3. def OAI.MetricKMedian.Completion.Rational.Program.Input.raw line 25
  4. def OAI.MetricKMedian.Completion.Rational.Program.Input.encode line 28
  5. def OAI.MetricKMedian.Completion.Rational.Program.Input.packing line 29
  6. def OAI.MetricKMedian.Completion.Rational.Program.packRaw line 31
  7. theorem OAI.MetricKMedian.Completion.Rational.Program.packRaw_poly line 33
  8. theorem OAI.MetricKMedian.Completion.Rational.Program.packRaw_input line 34
  9. def OAI.MetricKMedian.Completion.Rational.Program.packInputProgram line 39
  10. def OAI.MetricKMedian.Completion.Rational.Program.finish line 42
  11. theorem OAI.MetricKMedian.Completion.Rational.Program.finish_poly line 45
  12. theorem OAI.MetricKMedian.Completion.Rational.Program.finish_input line 55
  13. def OAI.MetricKMedian.Completion.Rational.Program.program line 86