OAI/Combinatorics/Progressions/Lattices/LatticeCoordinateLifts.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerCoordinateLattice line 20
  2. instance OAI.Erdos3.integerCoordinateLattice_discrete line 23
  3. instance OAI.Erdos3.integerCoordinateLattice_full line 27
  4. theorem OAI.Erdos3.mem_integerCoordinateLattice_iff line 30
  5. theorem OAI.Erdos3.integerCoordinateLattice_covolume line 44
  6. theorem OAI.Erdos3.integer_lattice_covolume_eq_index line 55
  7. theorem OAI.Erdos3.integer_lattice_index_pos line 62
  8. theorem OAI.Erdos3.integer_lattice_index_nsmul_mem line 70
  9. def OAI.Erdos3.integerVectorRealMap line 87
  10. theorem OAI.Erdos3.integerVectorRealMap_injective line 92
  11. def OAI.Erdos3.integerVectorRealEquiv line 100
  12. def OAI.Erdos3.cyclicIntegerKernel line 110
  13. theorem OAI.Erdos3.mem_cyclicIntegerKernel line 114
  14. theorem OAI.Erdos3.integerVectorRealMap_mem_cyclicIntegerKernel line 119
  15. theorem OAI.Erdos3.cyclicIntegerKernel_le_integerCoordinateLattice line 128
  16. instance OAI.Erdos3.cyclicIntegerKernel_discrete line 133
  17. theorem OAI.Erdos3.nsmul_integerVectorRealMap_mem_cyclicIntegerKernel line 142
  18. instance OAI.Erdos3.cyclicIntegerKernel_full line 148
  19. theorem OAI.Erdos3.cyclicIntegerKernel_covolume_eq_card_range line 172
  20. theorem OAI.Erdos3.cyclicIntegerKernel_covolume_le line 190
  21. def OAI.Erdos3.latticeImage line 212
  22. theorem OAI.Erdos3.latticeImage_le_integer line 214
  23. theorem OAI.Erdos3.latticeImage_discrete line 219
  24. theorem OAI.Erdos3.latticeImage_full line 226
  25. theorem OAI.Erdos3.latticeImage_index_lift line 234
  26. theorem OAI.Erdos3.latticeImage_index_pos line 239
  27. theorem OAI.Erdos3.lattice_basis_coordinates_bound line 257
  28. theorem OAI.Erdos3.basisFun_mem_realIntegerGrid line 319
  29. theorem OAI.Erdos3.latticeImage_basis_lifts line 325