OAI/Geometry/HeilbronnTriangle/ShortestIntegralVector.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem355.IntegralMinima.toEuclidean line 13
2. def OAI.Problem355.IntegralMinima.normSq line 16
3. lemma OAI.Problem355.IntegralMinima.norm_sq_eq line 18
4. lemma OAI.Problem355.IntegralMinima.norm_le_norm_iff line 30
5. theorem OAI.Problem355.IntegralMinima.exists_shortest line 35
6. theorem OAI.Problem355.IntegralMinima.one_le_norm line 46
7. theorem OAI.Problem355.IntegralMinima.exists_shortest_outside line 62
8. theorem OAI.Problem355.IntegralMinima.exists_shortest_outside_of_independent line 79
9. theorem OAI.Problem355.IntegralMinima.shortest_kernel_has_bezout line 112