OAI/GroupTheory/SimpleAmenable/Simplicial/FiniteSetMonoidal.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.toEquiv line 13
  2. instance OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.(instance at line 14) line 14
  3. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.hom_ext line 16
  4. abbrev OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.sum line 17
  5. abbrev OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.empty line 18
  6. def OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.sumEquiv line 19
  7. def OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.sumHom line 22
  8. def OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.assoc line 24
  9. def OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.swap line 29
  10. def OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.left line 31
  11. def OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.right line 33
  12. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.comp_eq line 35
  13. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.id_eq line 37
  14. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.comp_apply line 38
  15. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.id_apply line 40
  16. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.sumHom_inl line 41
  17. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.sumHom_inr line 43
  18. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.assoc_left line 45
  19. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.assoc_mid line 48
  20. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.assoc_right line 51
  21. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.swap_left line 54
  22. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.swap_right line 56
  23. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.left_apply line 58
  24. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.right_apply line 60
  25. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.sumHom_id line 62
  26. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.sumHom_comp line 66
  27. abbrev OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.monoidalStruct line 72
  28. instance OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.monoidal line 84
  29. theorem OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.assoc_symm_left line 144
  30. theorem OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.assoc_symm_mid line 148
  31. theorem OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.assoc_symm_right line 152
  32. theorem OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.associator_inv_apply line 157
  33. theorem OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.inv_arrow_apply line 163
  34. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.inv_eq line 168
  35. instance OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.braided line 173
  36. instance OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.symmetric line 210