OAI/Geometry/PeriodicTiling/WordAffine.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PeriodicTilingThree.allowed_affine line 12
  2. def OAI.PeriodicTilingThree.intColumn line 28
  3. theorem OAI.PeriodicTilingThree.intColumn_val line 31
  4. theorem OAI.PeriodicTilingThree.intColumn_cast line 35
  5. def OAI.PeriodicTilingThree.rawArray line 41
  6. theorem OAI.PeriodicTilingThree.rawArray_column line 44
  7. theorem OAI.PeriodicTilingThree.rawArray_ne_zero line 53
  8. structure OAI.PeriodicTilingThree.LineAffine line 58
  9. def OAI.PeriodicTilingThree.chooseLine line 65
  10. theorem OAI.PeriodicTilingThree.LineAffine.raw_agrees line 71
  11. theorem OAI.PeriodicTilingThree.clean_second_difference line 79
  12. theorem OAI.PeriodicTilingThree.affine_four_line_closure line 117
  13. theorem OAI.PeriodicTilingThree.global_affine_approximation line 192