OAI/Geometry/PeriodicTiling/ConfigurationDifferences.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.configDiff line 15
  2. theorem OAI.PeriodicTilingThree.configDiff_apply line 18
  3. theorem OAI.PeriodicTilingThree.configDiff_zero line 21
  4. theorem OAI.PeriodicTilingThree.configDiff_const line 25
  5. theorem OAI.PeriodicTilingThree.configDiff_add line 30
  6. theorem OAI.PeriodicTilingThree.configDiff_sub line 36
  7. theorem OAI.PeriodicTilingThree.configDiff_comm line 42
  8. theorem OAI.PeriodicTilingThree.configDiff_eq_zero_iff line 49
  9. theorem OAI.PeriodicTilingThree.configDiff_add_period line 59
  10. theorem OAI.PeriodicTilingThree.configDiff_preserves_period line 64
  11. theorem OAI.PeriodicTilingThree.configDiff_sum line 69
  12. def OAI.PeriodicTilingThree.configDiffs line 77
  13. theorem OAI.PeriodicTilingThree.configDiffs_nil line 81
  14. theorem OAI.PeriodicTilingThree.configDiffs_cons line 83
  15. theorem OAI.PeriodicTilingThree.configDiffs_zero line 86
  16. theorem OAI.PeriodicTilingThree.configDiff_configDiffs line 92
  17. theorem OAI.PeriodicTilingThree.configDiffs_add line 99
  18. theorem OAI.PeriodicTilingThree.configDiffs_sub line 105
  19. theorem OAI.PeriodicTilingThree.configDiffs_sum line 111
  20. theorem OAI.PeriodicTilingThree.configDiffs_eq_zero_of_mem line 120
  21. theorem OAI.PeriodicTilingThree.configDiffs_const line 130
  22. theorem OAI.PeriodicTilingThree.configDiffs_preserves_period line 138
  23. theorem OAI.PeriodicTilingThree.configDiffs_replicate line 144