OAI/Geometry/HeilbronnTriangle/LatticeLowerProduct.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem355.LatticeLowerProduct.volumeReal_fundamentalDomain_orthonormal line 17
2. theorem OAI.Problem355.LatticeLowerProduct.covolume_span_basis_le_prod_norm line 25
3. theorem OAI.Problem355.LatticeLowerProduct.covolume_mono_reverse line 41
4. theorem OAI.Problem355.LatticeLowerProduct.covolume_le_prod_norm line 58
5. theorem OAI.Problem355.LatticeLowerProduct.relIndex_span_basis_le line 68