OAI/Combinatorics/Progressions/Geometry/MinkowskiSecondBoxGlue.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BohrLattice.MinkowskiSecondBox.rawTailLift line 12
  2. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.deleteProjection_rawTailLift line 16
  3. def OAI.Erdos3.BohrLattice.MinkowskiSecondBox.matrixBasis line 34
  4. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.matrixBasis_apply line 39
  5. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.matrix_mulVec_intCastVec_mem_span line 47
  6. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.minkowskiSecondConstant_succ line 57
  7. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.exists_abs_apply_eq_norm line 66
  8. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.realBox_smul_one_eq_const line 76
  9. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.cube_has_successiveProductCertificate line 82
  10. def OAI.Erdos3.BohrLattice.MinkowskiSecondBox.roundedTailLift line 323
  11. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.deleteProjection_roundedTailLift line 330
  12. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.roundedTailLift_norm_le_two line 340
  13. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.rawTailLift_mem_of_columns_mem line 365
  14. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.roundedTailLift_mem_of_columns_mem line 386
  15. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.roundedTailLift_linearIndependent line 395