OAI/Geometry/HeilbronnTriangle/LatticeBox.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem355.LatticeBox.box line 12
  2. theorem OAI.Problem355.LatticeBox.mem_box line 15
  3. theorem OAI.Problem355.LatticeBox.card_box line 19
  4. theorem OAI.Problem355.LatticeBox.card_le_of_coord_bound line 25
  5. theorem OAI.Problem355.LatticeBox.int_abs_le_floor line 31
  6. theorem OAI.Problem355.LatticeBox.card_le_of_real_coord_bound line 40
  7. theorem OAI.Problem355.LatticeBox.card_le_twentyseven_mul_cube line 53
  8. theorem OAI.Problem355.LatticeBox.card_le_onehundredtwentyfive_mul_cube line 63
  9. def OAI.Problem355.LatticeBox.realVector line 73
  10. theorem OAI.Problem355.LatticeBox.abs_coord_le_norm line 76
  11. theorem OAI.Problem355.LatticeBox.card_le_of_norm_bound line 80
  12. theorem OAI.Problem355.LatticeBox.card_le_of_norm_bound_twice line 87