OAI/GroupTheory/SimpleAmenable/Configurations/PointwisePolygonTables.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.conditionalAlternatingHom line 16
  2. theorem OAI.SimpleAmenable.conditionalHom_disjoint_commute line 21
  3. structure OAI.SimpleAmenable.PolygonLabelling line 34
  4. def OAI.SimpleAmenable.PolygonLabelling.fiber line 38
  5. theorem OAI.SimpleAmenable.PolygonLabelling.fiber_disjoint line 41
  6. def OAI.SimpleAmenable.PolygonLabelling.permutationHom line 47
  7. theorem OAI.SimpleAmenable.PolygonLabelling.permutationHom_apply line 57
  8. def OAI.SimpleAmenable.PolygonLabelling.tableHom line 61
  9. theorem OAI.SimpleAmenable.PolygonLabelling.tableHom_single line 71
  10. theorem OAI.SimpleAmenable.PolygonLabelling.tableHom_permutation line 76
  11. theorem OAI.SimpleAmenable.PolygonLabelling.tableHom_apply line 92
  12. theorem OAI.SimpleAmenable.PolygonLabelling.tableHom_injective line 98
  13. def OAI.SimpleAmenable.polygonAssignment line 110
  14. theorem OAI.SimpleAmenable.polygonAssignment_fiber_mem line 115
  15. def OAI.SimpleAmenable.actualPolygonLabelling line 133
  16. theorem OAI.SimpleAmenable.actualPolygonLabelling_surjective line 144