OAI/Combinatorics/Progressions/Geometry/CoordinateMinorCovolume.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exterior_norm_eq_sqrt_gram line 12
2. theorem OAI.Erdos3.abs_coordinate_det_le_sqrt_gram line 22
3. theorem OAI.Erdos3.abs_lattice_basis_coordinate_det_le_covolume line 47
4. theorem OAI.Erdos3.abs_isometric_lattice_basis_det_le_covolume line 63