OAI/Geometry/PeriodicTiling/FullDifferencePartition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PeriodicTilingThree.Coloring line 16
  2. def OAI.PeriodicTilingThree.BadDifference line 18
  3. def OAI.PeriodicTilingThree.badDifferenceColorings line 21
  4. theorem OAI.PeriodicTilingThree.mem_badDifferenceColorings line 26
  5. theorem OAI.PeriodicTilingThree.badDifference_card_le line 31
  6. def OAI.PeriodicTilingThree.badDifferenceLabels line 57
  7. theorem OAI.PeriodicTilingThree.badDifferenceLabels_card line 61
  8. def OAI.PeriodicTilingThree.someBadDifferenceColorings line 65
  9. theorem OAI.PeriodicTilingThree.someBadDifferenceColorings_card_le line 68
  10. theorem OAI.PeriodicTilingThree.exists_coloring_nonzero_differences line 84
  11. theorem OAI.PeriodicTilingThree.exists_partition_of_nonzero_coloring line 117
  12. theorem OAI.PeriodicTilingThree.exists_fresh_prime_fullDifference_partition line 143