OAI/Combinatorics/KMedian/Programs/UnitRepresentativeProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Preparation.RationalUnitInput.Program.Raw line 15
  2. def OAI.MetricKMedian.Preparation.RationalUnitInput.Program.view line 16
  3. structure OAI.MetricKMedian.Preparation.RationalUnitInput.Program.Input line 19
  4. abbrev OAI.MetricKMedian.Preparation.RationalUnitInput.Program.Input.raw line 23
  5. abbrev OAI.MetricKMedian.Preparation.RationalUnitInput.Program.Input.encode line 24
  6. def OAI.MetricKMedian.Preparation.RationalUnitInput.Program.values line 26
  7. theorem OAI.MetricKMedian.Preparation.RationalUnitInput.Program.values_poly line 29
  8. theorem OAI.MetricKMedian.Preparation.RationalUnitInput.Program.values_view line 34
  9. def OAI.MetricKMedian.Preparation.RationalUnitInput.Program.Input.rep line 41
  10. def OAI.MetricKMedian.Preparation.RationalUnitInput.Program.repData line 43
  11. theorem OAI.MetricKMedian.Preparation.RationalUnitInput.Program.repData_poly line 45
  12. theorem OAI.MetricKMedian.Preparation.RationalUnitInput.Program.repData_view line 49
  13. def OAI.MetricKMedian.Preparation.RationalUnitInput.Program.repInputProgram line 58
  14. def OAI.MetricKMedian.Preparation.RationalUnitInput.Program.repProgram line 60
  15. def OAI.MetricKMedian.Preparation.RationalUnitInput.Program.ranks line 64
  16. theorem OAI.MetricKMedian.Preparation.RationalUnitInput.Program.ranks_poly line 65
  17. theorem OAI.MetricKMedian.Preparation.RationalUnitInput.Program.ranks_view line 66