OAI/Geometry/HyperbolicGroups/CoreWordGraph.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.CoreWordGraph.adj line 13
  2. def OAI.HyperbolicObstruction.CoreWordGraph.graph line 18
  3. lemma OAI.HyperbolicObstruction.CoreWordGraph.core_adj line 23
  4. lemma OAI.HyperbolicObstruction.CoreWordGraph.core_edge_mem line 32
  5. def OAI.HyperbolicObstruction.CoreWordGraph.projection line 41
  6. lemma OAI.HyperbolicObstruction.CoreWordGraph.oriented_adj line 45
  7. def OAI.HyperbolicObstruction.CoreWordGraph.label line 54
  8. lemma OAI.HyperbolicObstruction.CoreWordGraph.label_rev line 57
  9. lemma OAI.HyperbolicObstruction.CoreWordGraph.oriented_label line 65
  10. abbrev OAI.HyperbolicObstruction.CoreWordGraph.Fields line 75
  11. def OAI.HyperbolicObstruction.CoreWordGraph.path line 78
  12. lemma OAI.HyperbolicObstruction.CoreWordGraph.path_length line 87
  13. lemma OAI.HyperbolicObstruction.CoreWordGraph.path_word line 95
  14. def OAI.HyperbolicObstruction.CoreWordGraph.toMaster line 108
  15. lemma OAI.HyperbolicObstruction.CoreWordGraph.toMaster_fields line 112
  16. lemma OAI.HyperbolicObstruction.CoreWordGraph.toMaster_word line 122
  17. lemma OAI.HyperbolicObstruction.CoreWordGraph.cycle_length line 129