OAI/Geometry/PeriodicTiling/WordObstruction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PeriodicTilingThree.word_one_ne_two line 14
  2. theorem OAI.PeriodicTilingThree.word_two_ne_zero line 23
  3. def OAI.PeriodicTilingThree.smallColumn line 29
  4. def OAI.PeriodicTilingThree.fourColumn line 32
  5. theorem OAI.PeriodicTilingThree.small_affine_nonzero line 35
  6. theorem OAI.PeriodicTilingThree.exists_vertical_value line 45
  7. theorem OAI.PeriodicTilingThree.nonconstantColumns_iff_vertical_coefficient line 58
  8. theorem OAI.PeriodicTilingThree.prime_dvd_vertical_period line 91
  9. def OAI.PeriodicTilingThree.straighten line 128
  10. theorem OAI.PeriodicTilingThree.straighten_lineRule line 131
  11. theorem OAI.PeriodicTilingThree.straighten_nonconstantColumns_iff line 143
  12. theorem OAI.PeriodicTilingThree.straighten_verticalPeriod_iff line 156
  13. theorem OAI.PeriodicTilingThree.exists_straighten_affine line 168
  14. def OAI.PeriodicTilingThree.rescale line 186
  15. theorem OAI.PeriodicTilingThree.rescale_lineRule line 189
  16. theorem OAI.PeriodicTilingThree.exists_nonzero_affine_ne line 201
  17. def OAI.PeriodicTilingThree.fiberColumn line 224
  18. theorem OAI.PeriodicTilingThree.rescale_vertical_coefficient_ne_zero line 232
  19. theorem OAI.PeriodicTilingThree.no_positive_nat_vertical_period line 329
  20. theorem OAI.PeriodicTilingThree.no_positive_vertical_period line 361