OAI/Geometry/HeilbronnTriangle/LatticeCoordinates.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem355.LatticeCoordinates.relIndex_nsmul_mem_span line 13
  2. theorem OAI.Problem355.LatticeCoordinates.exists_integer_coordinates_of_mem_span line 19
  3. theorem OAI.Problem355.LatticeCoordinates.exists_integer_coordinates line 30
  4. theorem OAI.Problem355.LatticeCoordinates.coordinates_eq_scaled_mul_inv line 39
  5. theorem OAI.Problem355.LatticeCoordinates.coordinates_det line 47
  6. theorem OAI.Problem355.LatticeCoordinates.coordinates_injective line 58
  7. theorem OAI.Problem355.LatticeCoordinates.abs_det_le_factorial_prod line 65
  8. theorem OAI.Problem355.LatticeCoordinates.coordinate_abs_bound line 83
  9. theorem OAI.Problem355.LatticeCoordinates.coordinate_abs_bound_of_product_bound line 101
  10. theorem OAI.Problem355.LatticeCoordinates.integer_coordinates_entry_bound line 125
  11. theorem OAI.Problem355.LatticeCoordinates.exists_coordinate_family line 144
  12. theorem OAI.Problem355.LatticeCoordinates.coordinates_det_ne_zero line 169
  13. theorem OAI.Problem355.LatticeCoordinates.euclidean_norm_le_of_coord_bound line 179
  14. theorem OAI.Problem355.LatticeCoordinates.integer_coordinates_column_bound line 197
  15. theorem OAI.Problem355.LatticeCoordinates.exists_fixed_det_coordinate_family line 211