OAI/Geometry/HeilbronnTriangle/PlaneCovolume.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem355.Lattice.covolume_sq_eq_det_gram line 13
2. theorem OAI.Problem355.Lattice.covolume_eq_sqrt_det_gram line 30
3. theorem OAI.Problem355.Lattice.normal_smul_cross_eq_det_smul line 39
4. theorem OAI.Problem355.Lattice.cross_norm_eq_abs_det_mul_norm_div line 53
5. theorem OAI.Problem355.Lattice.det_gram_pair_eq_cross_norm_sq line 66
6. theorem OAI.Problem355.Lattice.covolume_eq_cross_norm line 76
7. theorem OAI.Problem355.Lattice.covolume_eq_abs_det_mul_norm_div line 90
8. theorem OAI.Problem355.Lattice.covolume_eq_index_mul_norm_div line 108
9. theorem OAI.Problem355.Lattice.abs_det_int_basis_eq_index line 123
10. theorem OAI.Problem355.Lattice.abs_det_sum_basis_eq_index line 135
11. theorem OAI.Problem355.Lattice.euclidean_covolume_eq_det line 149