OAI/GroupTheory/SimpleAmenable/Simplicial/TrajectoryReindexLabels.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.PolygonObject.Labelled.reindexLabel line 14
  2. def OAI.SimpleAmenable.PolygonObject.Labelled.initialDisplacement line 17
  3. lemma OAI.SimpleAmenable.PolygonObject.Labelled.representative_partialSum line 20
  4. lemma OAI.SimpleAmenable.PolygonObject.Labelled.reindexLabel_reduced line 25
  5. lemma OAI.SimpleAmenable.PolygonObject.Labelled.partialSum_reindexLabel line 29
  6. abbrev OAI.SimpleAmenable.PolygonObject.Labelled.vertexArrow line 36
  7. lemma OAI.SimpleAmenable.PolygonObject.Labelled.initial_baseArrow line 39
  8. lemma OAI.SimpleAmenable.PolygonObject.Labelled.vertexArrow_zero line 43
  9. lemma OAI.SimpleAmenable.PolygonObject.Labelled.vertexArrow_ladder line 44
  10. lemma OAI.SimpleAmenable.PolygonObject.Labelled.ladder_app line 51
  11. lemma OAI.SimpleAmenable.PolygonObject.Labelled.trajectoryShift_vertex line 56
  12. lemma OAI.SimpleAmenable.PolygonObject.Labelled.increments_vertex_reindex line 63
  13. def OAI.SimpleAmenable.PolygonObject.Labelled.reindexFunctor line 75
  14. lemma OAI.SimpleAmenable.PolygonObject.Labelled.reindexFunctor_arrow line 77
  15. abbrev OAI.SimpleAmenable.PolygonObject.Labelled.reindexInitial line 80
  16. lemma OAI.SimpleAmenable.PolygonObject.Labelled.reindexInitial_positional line 84
  17. lemma OAI.SimpleAmenable.PolygonObject.Labelled.reindexInitial_labels line 86
  18. def OAI.SimpleAmenable.PolygonObject.Labelled.reindexLadder line 98
  19. lemma OAI.SimpleAmenable.PolygonObject.Labelled.reindexLadder_zero line 102
  20. lemma OAI.SimpleAmenable.PolygonObject.Labelled.comp_inv_last line 104
  21. lemma OAI.SimpleAmenable.PolygonObject.Labelled.cancel_two_inverses line 109
  22. def OAI.SimpleAmenable.PolygonObject.Labelled.reindexStringIso line 114
  23. lemma OAI.SimpleAmenable.PolygonObject.Labelled.tensorLadder_vertex line 130
  24. lemma OAI.SimpleAmenable.PolygonObject.Labelled.tensorLadder_app line 142
  25. instance OAI.SimpleAmenable.PolygonObject.Labelled.reindexMonoidal line 148
  26. instance OAI.SimpleAmenable.PolygonObject.Labelled.reindexBraided line 150
  27. lemma OAI.SimpleAmenable.PolygonObject.Labelled.reindex_μ_arrow line 152
  28. instance OAI.SimpleAmenable.PolygonObject.Labelled.reindexStringMonoidal line 161