OAI/GroupTheory/UniversalGroup/CentralHNN.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Higman.CentralExtension line 11
  2. def OAI.Higman.CentralExtension.map line 18
  3. theorem OAI.Higman.CentralExtension.map_of line 24
  4. theorem OAI.Higman.CentralExtension.map_t line 28
  5. def OAI.Higman.CentralExtension.mapWord line 32
  6. theorem OAI.Higman.CentralExtension.mapWord_prod line 46
  7. theorem OAI.Higman.CentralExtension.map_injective line 52
  8. def OAI.Higman.CentralExtension.relation line 79
  9. theorem OAI.Higman.CentralExtension.con_finitelyNormallyGenerated line 82
  10. theorem OAI.Higman.CentralExtension.finitelyPresented line 131
  11. abbrev OAI.Higman.Double.Extension line 148
  12. def OAI.Higman.Double.first line 150
  13. def OAI.Higman.Double.second line 152
  14. def OAI.Higman.Double.subgroup line 155
  15. def OAI.Higman.Double.firstIn line 157
  16. def OAI.Higman.Double.secondIn line 160
  17. def OAI.Higman.Double.lamp line 165
  18. theorem OAI.Higman.Double.lamp_left line 173
  19. theorem OAI.Higman.Double.lamp_right line 176
  20. def OAI.Higman.Double.coordinate line 178
  21. def OAI.Higman.Double.wreathMap line 186
  22. theorem OAI.Higman.Double.wreathMap_first line 193
  23. theorem OAI.Higman.Double.wreathMap_second line 197
  24. theorem OAI.Higman.Double.subgroup_le_coordKer line 203
  25. def OAI.Higman.Double.read line 213
  26. theorem OAI.Higman.Double.read_first line 218
  27. theorem OAI.Higman.Double.read_second line 224