OAI/GroupTheory/SimpleAmenable/Configurations/TransitiveInduction.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.TransitiveInduction.permutationRep line 18
  2. lemma OAI.SimpleAmenable.TransitiveInduction.permutationRep_single line 23
  3. def OAI.SimpleAmenable.TransitiveInduction.pointMap line 27
  4. def OAI.SimpleAmenable.TransitiveInduction.toPermutation line 37
  5. theorem OAI.SimpleAmenable.TransitiveInduction.toPermutation_mk line 42
  6. lemma OAI.SimpleAmenable.TransitiveInduction.mk_same line 47
  7. def OAI.SimpleAmenable.TransitiveInduction.transport line 62
  8. theorem OAI.SimpleAmenable.TransitiveInduction.transport_spec line 63
  9. def OAI.SimpleAmenable.TransitiveInduction.fromPermutation line 66
  10. theorem OAI.SimpleAmenable.TransitiveInduction.fromPermutation_single line 71
  11. lemma OAI.SimpleAmenable.TransitiveInduction.from_to line 75
  12. lemma OAI.SimpleAmenable.TransitiveInduction.to_from line 86
  13. def OAI.SimpleAmenable.TransitiveInduction.iso line 94
  14. def OAI.SimpleAmenable.TransitiveInduction.homologyIso line 104
  15. def OAI.SimpleAmenable.PolygonPlacement.Configuration.listEquiv line 118
  16. theorem OAI.SimpleAmenable.PolygonPlacement.Configuration.listEquiv_apply_val line 134
  17. def OAI.SimpleAmenable.PolygonPlacement.Configuration.chainEquiv line 137
  18. theorem OAI.SimpleAmenable.PolygonPlacement.Configuration.chainEquiv_single_val line 141
  19. theorem OAI.SimpleAmenable.PolygonPlacement.Configuration.chainEquiv_intertwines line 148
  20. def OAI.SimpleAmenable.PolygonPlacement.Configuration.representationIso line 163
  21. def OAI.SimpleAmenable.PolygonPlacement.Configuration.columnHomologyIso line 168