OAI/Geometry/HeilbronnTriangle/IntegerSamplingGeometry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem355.IntegerSamplingGeometry.Column line 12
2. def OAI.Problem355.IntegerSamplingGeometry.realColumn line 14
3. def OAI.Problem355.IntegerSamplingGeometry.matrix line 17
4. lemma OAI.Problem355.IntegerSamplingGeometry.realColumn_inBox line 20
5. lemma OAI.Problem355.IntegerSamplingGeometry.project_realColumn line 39
6. lemma OAI.Problem355.IntegerSamplingGeometry.det_realColumn line 42
7. theorem OAI.Problem355.IntegerSamplingGeometry.project_area_lower_bound line 47
8. theorem OAI.Problem355.IntegerSamplingGeometry.smallTriangle_implies_small_det line 58
9. def OAI.Problem355.IntegerSamplingGeometry.BadDet line 71
10. lemma OAI.Problem355.IntegerSamplingGeometry.smallTriangle_implies_badDet line 77
11. def OAI.Problem355.IntegerSamplingGeometry.determinantMass line 85
12. theorem OAI.Problem355.IntegerSamplingGeometry.tripleMass_le_determinantMass line 91