OAI/GroupTheory/Hyperbolic/BasedWords.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release075.BlockPresentation.basePath line 9
2. theorem OAI.Release075.BlockPresentation.based_comp_formula line 14
3. theorem OAI.Release075.BlockPresentation.based_id_formula line 23
4. theorem OAI.Release075.BlockPresentation.based_eq_id line 29
5. theorem OAI.Release075.BlockPresentation.based_oriented_arrow line 34
6. theorem OAI.Release075.BlockPresentation.based_rawWord line 77
7. theorem OAI.Release075.BlockPresentation.rawWord_nullhomotopic line 99
8. def OAI.Release075.BlockPresentation.rawEdge line 117

   Source documentation

   The original oriented edges really are arrows in the symmetrified quiver.

   def rawEdge (e : d.OrientedEdge) :
       (show Quiver.Symmetrify d.Vertex from d.edgeTarget (d.flipEdge e)) ⟶
         (show Quiver.Symmetrify d.Vertex from d.edgeTarget e) := by
   …

9. theorem OAI.Release075.BlockPresentation.orientedLabel_rawEdge line 129
10. theorem OAI.Release075.BlockPresentation.WordPath.exists_raw line 134
11. theorem OAI.Release075.BlockPresentation.typed_nullword_lifted_fillable line 147
12. theorem OAI.Release075.BlockPresentation.wordValue_reverse line 160
13. theorem OAI.Release075.BlockPresentation.exists_based_word line 166
14. theorem OAI.Release075.BlockPresentation.WordPath.shift line 195
15. theorem OAI.Release075.BlockPresentation.WordPath.forget line 205
16. theorem OAI.Release075.BlockPresentation.WordPath.displacement line 212
17. theorem OAI.Release075.BlockPresentation.WordPath.liftWord_eq line 222
18. theorem OAI.Release075.BlockPresentation.lifted_closed_fillable line 231
19. theorem OAI.Release075.BlockPresentation.exists_lifted_path line 239
20. theorem OAI.Release075.BlockPresentation.boundary₁_wordChain line 244
21. def OAI.Release075.BlockPresentation.powerWord line 254
22. theorem OAI.Release075.BlockPresentation.powerWord_zero line 258
23. theorem OAI.Release075.BlockPresentation.powerWord_succ line 261
24. theorem OAI.Release075.BlockPresentation.powerWord_succ_left line 264
25. theorem OAI.Release075.BlockPresentation.powerWord_typed line 279
26. theorem OAI.Release075.BlockPresentation.powerWord_chain line 290
27. theorem OAI.Release075.BlockPresentation.powerWord_shift_rotate line 296
28. theorem OAI.Release075.BlockPresentation.powerWord_chain_norm line 308
29. theorem OAI.Release075.FullFilling.allTriangles_reword line 324
30. theorem OAI.Release075.FullFilling.faceChain_reword line 327