OAI/Combinatorics/Progressions/Lattices/ResidueRefinedPeriod.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.integerMatrixImage_index line 19
  2. theorem OAI.Erdos3.integerMatrixImage_det_smul line 32
  3. theorem OAI.Erdos3.integerMatrixImage_multiple_smul line 38
  4. theorem OAI.Erdos3.integerMatrixImage_natAbs_smul line 45
  5. def OAI.Erdos3.pivotFreeLattice line 59
  6. def OAI.Erdos3.pivotFullImage line 63
  7. def OAI.Erdos3.pivotFreeAdmissible line 67
  8. theorem OAI.Erdos3.pivotFreeAdmissible_iff line 71
  9. theorem OAI.Erdos3.pivotFreeAdmissible_coset line 80
  10. theorem OAI.Erdos3.pivotFullImage_iff line 94
  11. def OAI.Erdos3.pivotIntegerFiberEquiv line 104
  12. theorem OAI.Erdos3.pivotFreeLattice_index_mul line 131
  13. def OAI.Erdos3.integerScalarLattice line 144
  14. theorem OAI.Erdos3.integerScalarLattice_mem line 147
  15. theorem OAI.Erdos3.integerScalarLattice_index line 150
  16. theorem OAI.Erdos3.integerScalarLattice_le_pivotFreeLattice line 165
  17. theorem OAI.Erdos3.pivot_residue_index_identity line 174
  18. def OAI.Erdos3.integerLatticeResidue line 194
  19. def OAI.Erdos3.integerLatticeResidueFintype line 198
  20. theorem OAI.Erdos3.integerLatticeResidue_card line 207
  21. def OAI.Erdos3.integerScalarPeriodEquiv line 212
  22. theorem OAI.Erdos3.integerScalarPeriodEquiv_apply line 227
  23. def OAI.Erdos3.additiveResidueEquiv line 232
  24. def OAI.Erdos3.integerLatticeResidueEquiv line 251
  25. theorem OAI.Erdos3.integerLatticeResidueEquiv_symm_apply line 258
  26. def OAI.Erdos3.integerResidueMap line 272
  27. theorem OAI.Erdos3.integerResidueMap_apply line 277
  28. theorem OAI.Erdos3.integerResidueMap_surjective line 280
  29. theorem OAI.Erdos3.integerResidueMap_ker line 286
  30. theorem OAI.Erdos3.integerResidueMap_eq_iff line 301
  31. def OAI.Erdos3.pivotAdmissibleLatticeEquiv line 320
  32. def OAI.Erdos3.pivotFiberGridEquiv line 330
  33. theorem OAI.Erdos3.pivotFiberGridEquiv_free line 340
  34. theorem OAI.Erdos3.pivotFiberGrid_card_mul line 351
  35. theorem OAI.Erdos3.pivotFiberGrid_tsum line 359
  36. theorem OAI.Erdos3.pivotFiberGrid_tsum_real line 373
  37. def OAI.Erdos3.residueLatticeImage line 399
  38. theorem OAI.Erdos3.residueLatticeImage_comap line 402
  39. theorem OAI.Erdos3.residueLatticeImage_mem_iff line 408
  40. theorem OAI.Erdos3.residueLatticeImage_determines_lattice line 414
  41. theorem OAI.Erdos3.residueLatticeImage_index line 420
  42. theorem OAI.Erdos3.residueLatticeImage_card_mul_index line 431
  43. theorem OAI.Erdos3.residueLatticeImage_index_eq_div line 443
  44. def OAI.Erdos3.integerResidueMatrix line 460
  45. theorem OAI.Erdos3.integerResidueMap_mulVec line 463
  46. theorem OAI.Erdos3.integerMatrixResidue_mem line 469
  47. theorem OAI.Erdos3.integerMatrixResidue_image_eq line 481
  48. theorem OAI.Erdos3.integerMatrixImage_residue_iff line 488
  49. theorem OAI.Erdos3.integerMatrixImage_eq_of_residueMatrix line 495
  50. theorem OAI.Erdos3.integerResidueMatrix_eq_of_mod line 504
  51. theorem OAI.Erdos3.residueLatticeImage_index_le line 518
  52. theorem OAI.Erdos3.residueLatticeImage_real_index line 526
  53. def OAI.Erdos3.reducedIntegerMatrix line 547
  54. theorem OAI.Erdos3.reducedIntegerMatrix_bounds line 550
  55. theorem OAI.Erdos3.integerResidueMatrix_reduced line 556
  56. theorem OAI.Erdos3.reducedIntegerMatrix_residue line 562
  57. theorem OAI.Erdos3.exists_bounded_integerMap_residue_matrix line 569
  58. theorem OAI.Erdos3.integerResidueMatrix_eq_iff_dvd_sub line 589
  59. theorem OAI.Erdos3.integerResidueMatrix_reduce line 605
  60. def OAI.Erdos3.residueMatrixShift line 612
  61. theorem OAI.Erdos3.residueMatrixShift_spec line 616
  62. theorem OAI.Erdos3.residueMatrixShift_bound line 643
  63. def OAI.Erdos3.residueRefinedPeriod line 674
  64. theorem OAI.Erdos3.residueRefinedPeriod_pos line 677
  65. theorem OAI.Erdos3.stride_mul_dvd_residueRefinedPeriod line 682
  66. theorem OAI.Erdos3.residueRefinedPeriod_exp_bound line 691