OAI/Geometry/PeriodicTiling/CyclicShear.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.CyclicShear.low line 12
  2. theorem OAI.PeriodicTilingThree.CyclicShear.low_natCast line 15
  3. theorem OAI.PeriodicTilingThree.CyclicShear.low_intCast line 18
  4. def OAI.PeriodicTilingThree.CyclicShear.highInteger line 22
  5. theorem OAI.PeriodicTilingThree.CyclicShear.highInteger_modulus line 27
  6. def OAI.PeriodicTilingThree.CyclicShear.highMul line 33
  7. theorem OAI.PeriodicTilingThree.CyclicShear.highMul_intCast line 36
  8. theorem OAI.PeriodicTilingThree.CyclicShear.highMul_natCast line 40
  9. theorem OAI.PeriodicTilingThree.CyclicShear.highMul_apply line 44
  10. theorem OAI.PeriodicTilingThree.CyclicShear.highMul_val line 48
  11. theorem OAI.PeriodicTilingThree.CyclicShear.highMul_injective line 55
  12. theorem OAI.PeriodicTilingThree.CyclicShear.low_highMul line 63
  13. theorem OAI.PeriodicTilingThree.CyclicShear.mem_range_highMul_iff line 70
  14. theorem OAI.PeriodicTilingThree.CyclicShear.range_highMul line 84
  15. def OAI.PeriodicTilingThree.CyclicShear.highEquiv line 89
  16. theorem OAI.PeriodicTilingThree.CyclicShear.highEquiv_apply line 96
  17. def OAI.PeriodicTilingThree.CyclicShear.shear line 99
  18. theorem OAI.PeriodicTilingThree.CyclicShear.low_shear line 102
  19. theorem OAI.PeriodicTilingThree.CyclicShear.shear_injective line 108
  20. theorem OAI.PeriodicTilingThree.CyclicShear.shear_eq_zero_add line 114
  21. theorem OAI.PeriodicTilingThree.CyclicShear.shear_surjective_fiber line 118
  22. def OAI.PeriodicTilingThree.CyclicShear.shearEquiv line 130
  23. theorem OAI.PeriodicTilingThree.CyclicShear.shearEquiv_apply line 136
  24. theorem OAI.PeriodicTilingThree.CyclicShear.shear_add line 139
  25. theorem OAI.PeriodicTilingThree.CyclicShear.shear_source_add line 144