OAI/Geometry/PeriodicTiling/ShiftMultiplicity.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.shiftMultiplicity line 16
  2. def OAI.PeriodicTilingThree.shiftOmega line 23
  3. abbrev OAI.PeriodicTilingThree.ShiftIndex line 27
  4. def OAI.PeriodicTilingThree.shift line 30
  5. theorem OAI.PeriodicTilingThree.shiftMultiplicity_cast line 36
  6. theorem OAI.PeriodicTilingThree.shiftMultiplicity_zero line 47
  7. theorem OAI.PeriodicTilingThree.sum_shiftMultiplicity_fst line 51
  8. theorem OAI.PeriodicTilingThree.sum_shiftMultiplicity_snd line 71
  9. theorem OAI.PeriodicTilingThree.sum_shiftMultiplicity line 91
  10. theorem OAI.PeriodicTilingThree.card_shiftIndex line 97
  11. theorem OAI.PeriodicTilingThree.sum_shift line 102
  12. def OAI.PeriodicTilingThree.shiftFibreEquiv line 107
  13. theorem OAI.PeriodicTilingThree.card_shift_fibre line 122
  14. def OAI.PeriodicTilingThree.shiftFibreAEquiv line 127
  15. def OAI.PeriodicTilingThree.shiftFibreBEquiv line 143
  16. theorem OAI.PeriodicTilingThree.card_shift_fibreA line 159
  17. theorem OAI.PeriodicTilingThree.card_shift_fibreB line 168
  18. def OAI.PeriodicTilingThree.fibreOrderA line 183
  19. def OAI.PeriodicTilingThree.fibreOrderB line 187
  20. def OAI.PeriodicTilingThree.rhoA line 191
  21. def OAI.PeriodicTilingThree.rhoB line 194
  22. theorem OAI.PeriodicTilingThree.fibreOrderA_apply line 197
  23. theorem OAI.PeriodicTilingThree.fibreOrderB_apply line 204
  24. def OAI.PeriodicTilingThree.shiftOrderA line 211
  25. def OAI.PeriodicTilingThree.shiftOrderB line 215
  26. theorem OAI.PeriodicTilingThree.shiftOrderA_apply line 219
  27. theorem OAI.PeriodicTilingThree.shiftOrderB_apply line 225
  28. theorem OAI.PeriodicTilingThree.bijective_fibreOrderA line 231
  29. theorem OAI.PeriodicTilingThree.bijective_fibreOrderB line 241