OAI/Geometry/HeilbronnTriangle/LatticePacking.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem355.LatticePacking.card_mul_measure_le line 11
  2. theorem OAI.Problem355.LatticePacking.card_mul_measure_le_closedBall line 27
  3. theorem OAI.Problem355.LatticePacking.fundamentalDomain_subset_closedBall line 45
  4. theorem OAI.Problem355.LatticePacking.card_mul_measure_le_basis line 60
  5. theorem OAI.Problem355.LatticePacking.plane_card_mul_area_le line 73
  6. theorem OAI.Problem355.LatticePacking.card_le_relIndex_mul line 105
  7. theorem OAI.Problem355.LatticePacking.plane_card_le_of_short_basis line 147
  8. theorem OAI.Problem355.LatticePacking.plane_card_le_of_short_independent line 190
  9. theorem OAI.Problem355.LatticePacking.card_tuples_le_pow line 203
  10. theorem OAI.Problem355.LatticePacking.plane_spanning_triples_card_le line 221
  11. theorem OAI.Problem355.LatticePacking.affine_plane_card_le line 256
  12. theorem OAI.Problem355.LatticePacking.kernel_fiber_card_le line 294