OAI/Geometry/PeriodicTiling/SharedSeedInverse.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.SharedSeed.sourceResidueEquiv line 14
  2. theorem OAI.PeriodicTilingThree.SharedSeed.sourceResidueEquiv_apply line 20
  3. theorem OAI.PeriodicTilingThree.SharedSeed.sourceResidueEquiv_symm_apply line 23
  4. def OAI.PeriodicTilingThree.SharedSeed.usefulOne line 26
  5. def OAI.PeriodicTilingThree.SharedSeed.highOne line 31
  6. def OAI.PeriodicTilingThree.SharedSeed.usefulTwo line 35
  7. def OAI.PeriodicTilingThree.SharedSeed.highTwo line 40
  8. def OAI.PeriodicTilingThree.SharedSeed.oneForward line 45
  9. def OAI.PeriodicTilingThree.SharedSeed.twoForward line 55
  10. def OAI.PeriodicTilingThree.SharedSeed.oneActivationEquiv line 65
  11. def OAI.PeriodicTilingThree.SharedSeed.twoActivationEquiv line 81
  12. theorem OAI.PeriodicTilingThree.SharedSeed.oneActivationEquiv_apply line 97
  13. theorem OAI.PeriodicTilingThree.SharedSeed.twoActivationEquiv_apply line 131
  14. theorem OAI.PeriodicTilingThree.SharedSeed.oneForward_bijective line 165
  15. theorem OAI.PeriodicTilingThree.SharedSeed.twoForward_bijective line 179