OAI/Combinatorics/Progressions/Estimates/MinkowskiSecondInduction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.BohrLattice.MinkowskiDiagonalNormalization.divideCoordinates line 14
2. theorem OAI.Erdos3.BohrLattice.MinkowskiDiagonalNormalization.divideCoordinates_apply line 31
3. theorem OAI.Erdos3.BohrLattice.MinkowskiDiagonalNormalization.divideCoordinates_symm_apply line 35
4. def OAI.Erdos3.BohrLattice.MinkowskiDiagonalNormalization.normalizedBasis line 39
5. theorem OAI.Erdos3.BohrLattice.MinkowskiDiagonalNormalization.normalizedBasis_apply line 44
6. theorem OAI.Erdos3.BohrLattice.MinkowskiDiagonalNormalization.mem_realBox_mul_iff line 50
7. theorem OAI.Erdos3.BohrLattice.MinkowskiDiagonalNormalization.abs_det_normalizedBasis line 72
8. theorem OAI.Erdos3.BohrLattice.MinkowskiDiagonalNormalization.divideCoordinates_mem_span_iff line 91
9. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.realBox_has_minkowskiSecondCertificate line 126