OAI/GroupTheory/SimpleAmenable/Simplicial/UniformMonoidal.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SimpleAmenable.PolygonObject.Labelled.objectUniform_sum line 17
  2. lemma OAI.SimpleAmenable.PolygonObject.Labelled.arrowUniform_sum line 24
  3. lemma OAI.SimpleAmenable.PolygonObject.Labelled.relabel_uniform line 57
  4. lemma OAI.SimpleAmenable.PolygonObject.Labelled.assocHom_uniform line 66
  5. lemma OAI.SimpleAmenable.PolygonObject.Labelled.swapHom_uniform line 81
  6. lemma OAI.SimpleAmenable.PolygonObject.Labelled.leftHom_uniform line 88
  7. lemma OAI.SimpleAmenable.PolygonObject.Labelled.rightHom_uniform line 97
  8. lemma OAI.SimpleAmenable.PolygonObject.Labelled.sumHom_id line 107
  9. abbrev OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.sum line 114
  10. abbrev OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.empty line 122
  11. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.sumHom line 127
  12. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.assocHom line 130
  13. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.leftHom line 132
  14. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.rightHom line 134
  15. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.swapHom line 136
  16. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.(instance at line 139) line 139
  17. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.inducing line 149
  18. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.(instance at line 170) line 170
  19. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.(instance at line 171) line 171
  20. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.(instance at line 174) line 174
  21. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.(instance at line 179) line 179
  22. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.(instance at line 183) line 183