OAI/Geometry/HeilbronnTriangle/IntegralAmbientLattice.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Problem355.IntegralPlaneLattice.standardLattice_isZLattice line 10
2. lemma OAI.Problem355.IntegralPlaneLattice.castLinear_injective line 14
3. lemma OAI.Problem355.IntegralPlaneLattice.realLattice_top line 21
4. lemma OAI.Problem355.IntegralPlaneLattice.realLattice_spans line 29
5. lemma OAI.Problem355.IntegralPlaneLattice.realLattice_isZLattice line 48
6. lemma OAI.Problem355.IntegralPlaneLattice.standardLattice_covolume line 52
7. lemma OAI.Problem355.IntegralPlaneLattice.realLattice_relIndex line 60
8. lemma OAI.Problem355.IntegralPlaneLattice.one_le_norm_of_mem_standardLattice line 69
9. lemma OAI.Problem355.IntegralPlaneLattice.one_le_norm_of_mem_realLattice line 88
10. lemma OAI.Problem355.IntegralPlaneLattice.realLattice_covolume line 92