OAI/GroupTheory/SimpleAmenable/CentralCovers/GenuineFiniteGeneration.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.fiveTrackBoolean_polygon line 17
  2. theorem OAI.SimpleAmenable.fiveTrack_polygon_generated line 36
  3. theorem OAI.SimpleAmenable.extend_three_tracks line 43
  4. theorem OAI.SimpleAmenable.trackCycle_viaEmbedding line 65
  5. theorem OAI.SimpleAmenable.conditional_cycle_generated line 83
  6. def OAI.SimpleAmenable.offsetFrame line 97
  7. theorem OAI.SimpleAmenable.offsetFrame_apply line 101
  8. theorem OAI.SimpleAmenable.offsetFrame_generated line 112
  9. theorem OAI.SimpleAmenable.distinct_track_cycle_generated line 123
  10. def OAI.SimpleAmenable.starThreeInFive line 189
  11. theorem OAI.SimpleAmenable.star_cycle_identity line 192
  12. theorem OAI.SimpleAmenable.threeSlot_generated line 197
  13. theorem OAI.SimpleAmenable.sourceGenerated_eq_alternating line 223
  14. theorem OAI.SimpleAmenable.polygonAlternatingGroup_fg line 230
  15. theorem OAI.SimpleAmenable.alternatingGenerator_surjective line 238
  16. theorem OAI.SimpleAmenable.sourceCover_surjective line 251
  17. theorem OAI.SimpleAmenable.sourceCover_eventually_perfect line 256