OAI/Geometry/PeriodicTiling/CyclicQuotient.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PeriodicTilingThree.CyclicQuotient.Group line 12
  2. def OAI.PeriodicTilingThree.CyclicQuotient.projection line 14
  3. def OAI.PeriodicTilingThree.CyclicQuotient.kernelStep line 19
  4. theorem OAI.PeriodicTilingThree.CyclicQuotient.projection_kernelStep line 21
  5. theorem OAI.PeriodicTilingThree.CyclicQuotient.kernelStep_ne_zero line 25
  6. def OAI.PeriodicTilingThree.CyclicQuotient.lift line 31
  7. theorem OAI.PeriodicTilingThree.CyclicQuotient.projection_lift line 34
  8. theorem OAI.PeriodicTilingThree.CyclicQuotient.lift_zero line 39
  9. theorem OAI.PeriodicTilingThree.CyclicQuotient.projection_surjective line 43
  10. theorem OAI.PeriodicTilingThree.CyclicQuotient.lift_injective line 47
  11. theorem OAI.PeriodicTilingThree.CyclicQuotient.mem_ker_iff_zsmul_kernelStep line 52
  12. def OAI.PeriodicTilingThree.CyclicQuotient.representatives line 68
  13. theorem OAI.PeriodicTilingThree.CyclicQuotient.lift_mem_representatives line 71
  14. theorem OAI.PeriodicTilingThree.CyclicQuotient.projection_mem_of_mem_representatives line 75
  15. theorem OAI.PeriodicTilingThree.CyclicQuotient.projection_injOn_representatives line 81
  16. theorem OAI.PeriodicTilingThree.CyclicQuotient.projection_image_representatives line 90
  17. theorem OAI.PeriodicTilingThree.CyclicQuotient.zero_mem_representatives line 103
  18. theorem OAI.PeriodicTilingThree.CyclicQuotient.eq_zero_of_mem_representatives_mem_ker line 107
  19. theorem OAI.PeriodicTilingThree.CyclicQuotient.kernelStep_not_mem_representatives line 115
  20. theorem OAI.PeriodicTilingThree.CyclicQuotient.preimage_tiles line 121
  21. theorem OAI.PeriodicTilingThree.CyclicQuotient.period_preimage_of_mem_ker line 141
  22. theorem OAI.PeriodicTilingThree.CyclicQuotient.period_preimage_kernelStep line 149