OAI/GroupTheory/UniversalGroup/Benign.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Higman.HNN.conj_mem_range_iff line 12
  2. theorem OAI.Higman.HNN.commute_t_iff line 29
  3. theorem OAI.Higman.benign_iff_centralExtension_embeds line 44
  4. theorem OAI.Higman.embeds_of_benign_kernel_fp line 95
  5. abbrev OAI.Higman.CentralExtension.rawProjection line 113
  6. theorem OAI.Higman.CentralExtension.rawProjection_ker line 116
  7. theorem OAI.Higman.CentralExtension.rawMap_surjective line 145
  8. theorem OAI.Higman.CentralExtension.rawProjection_ker_map line 156
  9. theorem OAI.Higman.IsBenign.map_surjective line 179
  10. def OAI.Higman.HNNTransport.map line 225
  11. theorem OAI.Higman.HNNTransport.map_of line 231
  12. theorem OAI.Higman.HNNTransport.map_t line 234
  13. def OAI.Higman.HNNTransport.mapWord line 236
  14. theorem OAI.Higman.HNNTransport.mapWord_prod line 252
  15. theorem OAI.Higman.HNNTransport.mem_base_of_map_mem_base line 258
  16. theorem OAI.Higman.HNNTransport.map_injective line 275
  17. theorem OAI.Higman.HNNTransport.range_comap_of line 290
  18. def OAI.Higman.HNNSubgroup.restricted line 309
  19. def OAI.Higman.HNNSubgroup.inclusion line 317
  20. theorem OAI.Higman.HNNSubgroup.inclusion_of line 321
  21. theorem OAI.Higman.HNNSubgroup.inclusion_t line 325
  22. theorem OAI.Higman.HNNSubgroup.range_comap_of line 328
  23. theorem OAI.Higman.HNNSubgroup.closure_comap_of line 334