OAI/Geometry/PeriodicTiling/ResidueCoordinates.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PeriodicTilingThree.Residue3 line 12
  2. abbrev OAI.PeriodicTilingThree.LiftAlphabet line 13
  3. abbrev OAI.PeriodicTilingThree.LiftAssignment line 14
  4. def OAI.PeriodicTilingThree.residueMod line 16
  5. def OAI.PeriodicTilingThree.can line 18
  6. def OAI.PeriodicTilingThree.signed line 20
  7. def OAI.PeriodicTilingThree.representative line 22
  8. theorem OAI.PeriodicTilingThree.residueMod_can line 26
  9. theorem OAI.PeriodicTilingThree.representative_residue line 31
  10. theorem OAI.PeriodicTilingThree.representative_injective line 37
  11. theorem OAI.PeriodicTilingThree.can_nonneg line 43
  12. theorem OAI.PeriodicTilingThree.can_lt line 47
  13. theorem OAI.PeriodicTilingThree.signed_bounds line 52
  14. def OAI.PeriodicTilingThree.Requested line 58
  15. def OAI.PeriodicTilingThree.requestedVectors line 61
  16. theorem OAI.PeriodicTilingThree.mem_requestedVectors line 66
  17. theorem OAI.PeriodicTilingThree.card_requestedVectors_le line 72
  18. theorem OAI.PeriodicTilingThree.requested_residueMod_ne_zero line 84
  19. theorem OAI.PeriodicTilingThree.requested_successor_ne line 92
  20. theorem OAI.PeriodicTilingThree.card_residue3 line 99
  21. theorem OAI.PeriodicTilingThree.card_liftAlphabet line 102
  22. theorem OAI.PeriodicTilingThree.card_liftAlphabet_pairs line 105
  23. def OAI.PeriodicTilingThree.liftDifference line 108
  24. theorem OAI.PeriodicTilingThree.liftDifference_eq line 111
  25. theorem OAI.PeriodicTilingThree.liftDifference_bounds line 122