OAI/GroupTheory/Hyperbolic/FullChains.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release075.BlockPresentation.shiftEdge line 9
  2. def OAI.Release075.BlockPresentation.shiftVertex line 10
  3. theorem OAI.Release075.BlockPresentation.shiftEdge_one line 12
  4. theorem OAI.Release075.BlockPresentation.shiftEdge_mul line 15
  5. theorem OAI.Release075.BlockPresentation.shiftEdge_flip line 19
  6. theorem OAI.Release075.BlockPresentation.shiftEdge_target line 23
  7. theorem OAI.Release075.BlockPresentation.LiftedFace.shift line 26
  8. theorem OAI.Release075.BlockPresentation.edgeChain_shift line 34
  9. theorem OAI.Release075.BlockPresentation.positiveAtom_shift line 40
  10. theorem OAI.Release075.BlockPresentation.orderedEval_shift line 47
  11. theorem OAI.Release075.BlockPresentation.faceEval_shift line 52
  12. theorem OAI.Release075.BlockPresentation.boundary₁_shift line 57
  13. theorem OAI.Release075.BlockPresentation.boundary₂_shift line 66
  14. theorem OAI.Release075.BlockPresentation.augmentation_boundary₁ line 77
  15. theorem OAI.Release075.BlockPresentation.wordChain_append line 85
  16. theorem OAI.Release075.BlockPresentation.wordChain_shift line 89
  17. def OAI.Release075.FullFilling.AllTriangles line 100
  18. def OAI.Release075.FullFilling.faceChain line 103
  19. theorem OAI.Release075.FullFilling.triple_faceChain line 105
  20. theorem OAI.Release075.FullFilling.boundary₂_faceChain line 110
  21. abbrev OAI.Release075.FullFilling.shift line 126
  22. theorem OAI.Release075.FullFilling.allTriangles_shift line 148
  23. theorem OAI.Release075.FullFilling.allTriangles_rotate line 151
  24. theorem OAI.Release075.FullFilling.faceChain_rotate line 155
  25. theorem OAI.Release075.FullFilling.faceChain_shift line 158
  26. theorem OAI.Release075.MarkedLineData.fullChain_unique line 178