OAI/Geometry/PeriodicTiling/CyclicStack.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PeriodicTilingThree.not_dvd_card_of_lt line 10
  2. theorem OAI.PeriodicTilingThree.cyclicStackOrder_pos line 15
  3. def OAI.PeriodicTilingThree.freshCyclicEquiv line 19
  4. def OAI.PeriodicTilingThree.cyclicStackEquiv line 34
  5. theorem OAI.PeriodicTilingThree.cyclicStackEquiv_fst line 43
  6. def OAI.PeriodicTilingThree.cyclicStackComplement line 54
  7. def OAI.PeriodicTilingThree.cyclicStackProjection line 58
  8. theorem OAI.PeriodicTilingThree.fullyPeriodic_cyclicStackComplement line 62
  9. theorem OAI.PeriodicTilingThree.fullyPeriodic_cyclicStackProjection line 69
  10. def OAI.PeriodicTilingThree.cyclicStackTile line 85
  11. theorem OAI.PeriodicTilingThree.tiles_cyclicStackTile line 92
  12. theorem OAI.PeriodicTilingThree.tiles_stack_of_tiles_cyclicStackTile line 103
  13. theorem OAI.PeriodicTilingThree.tiles_of_tiles_cyclicStackTile line 114
  14. theorem OAI.PeriodicTilingThree.cyclicStack_counterexample_of_common_system line 126