OAI/Geometry/PeriodicTiling/SharedSeedRegions.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PeriodicTilingThree.SharedSeed.Residues line 18
  2. abbrev OAI.PeriodicTilingThree.SharedSeed.ActiveLabels line 19
  3. abbrev OAI.PeriodicTilingThree.SharedSeed.InactiveLabels line 20
  4. abbrev OAI.PeriodicTilingThree.SharedSeed.LabelledResidue line 21
  5. def OAI.PeriodicTilingThree.SharedSeed.residue line 24
  6. def OAI.PeriodicTilingThree.SharedSeed.firstPoint line 26
  7. def OAI.PeriodicTilingThree.SharedSeed.secondPoint line 29
  8. def OAI.PeriodicTilingThree.SharedSeed.activePoint line 32
  9. def OAI.PeriodicTilingThree.SharedSeed.firstRegion line 35
  10. def OAI.PeriodicTilingThree.SharedSeed.secondRegion line 36
  11. def OAI.PeriodicTilingThree.SharedSeed.Rest line 37
  12. def OAI.PeriodicTilingThree.SharedSeed.copyCount line 38
  13. theorem OAI.PeriodicTilingThree.SharedSeed.nat_multiple_cast_injective line 40
  14. theorem OAI.PeriodicTilingThree.SharedSeed.firstPoint_injective line 53
  15. theorem OAI.PeriodicTilingThree.SharedSeed.secondPoint_injective line 62
  16. theorem OAI.PeriodicTilingThree.SharedSeed.firstPoint_ne_secondPoint line 77
  17. theorem OAI.PeriodicTilingThree.SharedSeed.activePoint_injective line 91
  18. theorem OAI.PeriodicTilingThree.SharedSeed.first_second_disjoint line 104
  19. theorem OAI.PeriodicTilingThree.SharedSeed.seven_le_pow line 110
  20. theorem OAI.PeriodicTilingThree.SharedSeed.pow_four_mod_six line 114
  21. theorem OAI.PeriodicTilingThree.SharedSeed.six_dvd_remainder line 126
  22. theorem OAI.PeriodicTilingThree.SharedSeed.copyCount_mul_six line 133
  23. theorem OAI.PeriodicTilingThree.SharedSeed.six_mul_copyCount_add_seven line 137
  24. def OAI.PeriodicTilingThree.SharedSeed.restEquiv line 143
  25. def OAI.PeriodicTilingThree.SharedSeed.residueAssembly line 162
  26. def OAI.PeriodicTilingThree.SharedSeed.residueEquiv line 171
  27. theorem OAI.PeriodicTilingThree.SharedSeed.residueAssembly_first line 175
  28. theorem OAI.PeriodicTilingThree.SharedSeed.residueAssembly_second line 179
  29. theorem OAI.PeriodicTilingThree.SharedSeed.residueEquiv_firstPoint line 183
  30. theorem OAI.PeriodicTilingThree.SharedSeed.residueEquiv_secondPoint line 188
  31. theorem OAI.PeriodicTilingThree.SharedSeed.residueEquiv_first_iff line 193
  32. theorem OAI.PeriodicTilingThree.SharedSeed.residueEquiv_second_iff line 204
  33. def OAI.PeriodicTilingThree.SharedSeed.reduce line 216
  34. theorem OAI.PeriodicTilingThree.SharedSeed.reduce_firstPoint line 220
  35. theorem OAI.PeriodicTilingThree.SharedSeed.reduce_secondPoint line 230
  36. theorem OAI.PeriodicTilingThree.SharedSeed.reduce_of_firstRegion line 240
  37. theorem OAI.PeriodicTilingThree.SharedSeed.reduce_of_secondRegion line 245
  38. def OAI.PeriodicTilingThree.SharedSeed.outputEquiv line 250