OAI/Geometry/PeriodicTiling/ActivationOffsets.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.separatedResidueLift line 16
  2. theorem OAI.PeriodicTilingThree.separatedResidueLift_cast line 20
  3. theorem OAI.PeriodicTilingThree.separatedResidueLift_injective line 25
  4. abbrev OAI.PeriodicTilingThree.ActivationIndex line 47
  5. abbrev OAI.PeriodicTilingThree.SeedActivationIndex line 50
  6. def OAI.PeriodicTilingThree.otherSeed line 52
  7. theorem OAI.PeriodicTilingThree.otherSeed_ne_self line 54
  8. theorem OAI.PeriodicTilingThree.otherSeed_otherSeed line 57
  9. def OAI.PeriodicTilingThree.activationModulus line 60
  10. instance OAI.PeriodicTilingThree.activationModulus_neZero line 62
  11. theorem OAI.PeriodicTilingThree.activationCoprime line 66
  12. def OAI.PeriodicTilingThree.activationCRT line 71
  13. def OAI.PeriodicTilingThree.activationResidue line 77
  14. def OAI.PeriodicTilingThree.ordinaryFirst line 83
  15. def OAI.PeriodicTilingThree.ordinaryOffset line 86
  16. theorem OAI.PeriodicTilingThree.ordinaryFirst_residues line 89
  17. theorem OAI.PeriodicTilingThree.ordinaryOffset_low line 107
  18. theorem OAI.PeriodicTilingThree.ordinaryOffset_rhoA line 111
  19. theorem OAI.PeriodicTilingThree.ordinaryOffset_rhoB line 116
  20. theorem OAI.PeriodicTilingThree.ordinaryOffset_lineValue line 121
  21. theorem OAI.PeriodicTilingThree.ordinaryOffset_injective line 125
  22. def OAI.PeriodicTilingThree.seedModulus line 129
  23. instance OAI.PeriodicTilingThree.seedModulus_neZero line 132
  24. theorem OAI.PeriodicTilingThree.activationCoprime_p line 136
  25. theorem OAI.PeriodicTilingThree.seedCoprime_other line 143
  26. def OAI.PeriodicTilingThree.seedCRT line 155
  27. def OAI.PeriodicTilingThree.seedActivationResidue line 165
  28. def OAI.PeriodicTilingThree.seedFirst line 171
  29. def OAI.PeriodicTilingThree.seedOffset line 174
  30. theorem OAI.PeriodicTilingThree.seedFirst_residues line 177
  31. theorem OAI.PeriodicTilingThree.seedOffset_low line 200
  32. theorem OAI.PeriodicTilingThree.seedOffset_rhoA line 204
  33. theorem OAI.PeriodicTilingThree.seedOffset_rhoB line 209
  34. theorem OAI.PeriodicTilingThree.seedOffset_other line 214
  35. theorem OAI.PeriodicTilingThree.seedOffset_residue line 218
  36. theorem OAI.PeriodicTilingThree.seedOffset_injective line 225