OAI/Geometry/HeilbronnTriangle/IntegerMatrixTransport.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem355.IntegerMatrixTransport.IntMatrix line 13
  2. abbrev OAI.Problem355.IntegerMatrixTransport.Triple line 14
  3. theorem OAI.Problem355.IntegerMatrixTransport.integralMatrix_injective line 16
  4. def OAI.Problem355.IntegerMatrixTransport.matrixFamily line 23
  5. theorem OAI.Problem355.IntegerMatrixTransport.mem_matrixFamily line 28
  6. theorem OAI.Problem355.IntegerMatrixTransport.card_matrixFamily line 34
  7. theorem OAI.Problem355.IntegerMatrixTransport.sum_matrixFamily line 39
  8. theorem OAI.Problem355.IntegerMatrixTransport.matrixFamily_filter line 45
  9. theorem OAI.Problem355.IntegerMatrixTransport.sum_matrixFamily_filter line 58
  10. theorem OAI.Problem355.IntegerMatrixTransport.entry_bounds line 66
  11. theorem OAI.Problem355.IntegerMatrixTransport.height_bounds line 73
  12. theorem OAI.Problem355.IntegerMatrixTransport.height_ne_zero line 80
  13. theorem OAI.Problem355.IntegerMatrixTransport.abs_entry_le line 85
  14. theorem OAI.Problem355.IntegerMatrixTransport.abs_real_entry_le line 90
  15. theorem OAI.Problem355.IntegerMatrixTransport.projectedColumn_eq line 94
  16. theorem OAI.Problem355.IntegerMatrixTransport.reduction_transpose line 98
  17. theorem OAI.Problem355.IntegerMatrixTransport.mem_orbit_iff_reduction_mem_slOrbit line 103
  18. theorem OAI.Problem355.IntegerMatrixTransport.rows_mem_integerRowLattice line 120
  19. theorem OAI.Problem355.IntegerMatrixTransport.determinant_residue line 128
  20. theorem OAI.Problem355.IntegerMatrixTransport.auxiliaryWeight_integralMatrix line 136
  21. def OAI.Problem355.IntegerMatrixTransport.samplingMatrices line 143
  22. theorem OAI.Problem355.IntegerMatrixTransport.mem_matrixFamily_univ_iff line 146
  23. theorem OAI.Problem355.IntegerMatrixTransport.mem_samplingMatrices_iff line 157
  24. theorem OAI.Problem355.IntegerMatrixTransport.matrixFamily_subset_samplingMatrices line 173
  25. def OAI.Problem355.IntegerMatrixTransport.matrixFiber line 180
  26. theorem OAI.Problem355.IntegerMatrixTransport.mem_matrixFiber line 187
  27. theorem OAI.Problem355.IntegerMatrixTransport.matrixFiber_properties line 200
  28. theorem OAI.Problem355.IntegerMatrixTransport.sum_matrixFiber line 210
  29. theorem OAI.Problem355.IntegerMatrixTransport.projected_pairwise_of_three line 225
  30. theorem OAI.Problem355.IntegerMatrixTransport.matrixFiber_projected_pairwise line 239