OAI/GroupTheory/SimpleAmenable/PolygonGeometry/ShiftedSlots.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.supported_inv line 12
  2. theorem OAI.SimpleAmenable.slotHom_supported line 19
  3. theorem OAI.SimpleAmenable.SupportedIn.mono line 26
  4. theorem OAI.SimpleAmenable.subslots_injective line 30
  5. theorem OAI.SimpleAmenable.slotHom_subcycle line 38
  6. theorem OAI.SimpleAmenable.relative_normal_commutator_mem line 67
  7. theorem OAI.SimpleAmenable.displaced_five_slot_cycle_mem line 76
  8. theorem OAI.SimpleAmenable.polygon_separates line 105
  9. theorem OAI.SimpleAmenable.exists_displaced_polygon line 127
  10. def OAI.SimpleAmenable.shiftedSlots line 168
  11. theorem OAI.SimpleAmenable.untranslate_mem line 172
  12. theorem OAI.SimpleAmenable.slotMap_shifted line 180
  13. theorem OAI.SimpleAmenable.shiftedSlots_injective line 187
  14. theorem OAI.SimpleAmenable.threeSlot_eq_slotHom line 198
  15. theorem OAI.SimpleAmenable.alternating_le_of_nontrivial_relative_normal line 216
  16. theorem OAI.SimpleAmenable.polygonAlternatingGroup_simple line 253