OAI/GroupTheory/UniversalGroup/RopeTrick.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Higman.commute_of_free_generators line 10
  2. theorem OAI.Higman.finitelyPresented_prod line 33
  3. abbrev OAI.Higman.RopeTrick.Raw line 84
  4. def OAI.Higman.RopeTrick.rawK line 86
  5. def OAI.Higman.RopeTrick.rawF line 87
  6. def OAI.Higman.RopeTrick.rawT line 88
  7. def OAI.Higman.RopeTrick.relation line 90
  8. abbrev OAI.Higman.RopeTrick.relations line 96
  9. abbrev OAI.Higman.RopeTrick.Container line 97
  10. def OAI.Higman.RopeTrick.proj line 99
  11. def OAI.Higman.RopeTrick.kMap line 101
  12. def OAI.Higman.RopeTrick.fMap line 102
  13. def OAI.Higman.RopeTrick.stable line 103
  14. theorem OAI.Higman.RopeTrick.finitelyPresented line 105
  15. lemma OAI.Higman.RopeTrick.relation_zero line 110
  16. lemma OAI.Higman.RopeTrick.generator_zero line 114
  17. lemma OAI.Higman.RopeTrick.generator_one line 121
  18. lemma OAI.Higman.RopeTrick.conjugate_zero line 128
  19. lemma OAI.Higman.RopeTrick.pair_eq line 139
  20. lemma OAI.Higman.RopeTrick.conjugate_one line 146
  21. lemma OAI.Higman.RopeTrick.kills_relation line 162
  22. def OAI.Higman.RopeTrick.left line 173
  23. def OAI.Higman.RopeTrick.right line 174
  24. lemma OAI.Higman.RopeTrick.left_injective line 177
  25. lemma OAI.Higman.RopeTrick.right_injective line 181
  26. def OAI.Higman.RopeTrick.associated line 185
  27. abbrev OAI.Higman.RopeTrick.Model line 189
  28. lemma OAI.Higman.RopeTrick.associated_left line 191
  29. lemma OAI.Higman.RopeTrick.model_relation line 199
  30. def OAI.Higman.RopeTrick.evaluate line 215
  31. lemma OAI.Higman.RopeTrick.evaluate_rawK line 219
  32. lemma OAI.Higman.RopeTrick.evaluate_rawF line 222
  33. lemma OAI.Higman.RopeTrick.evaluate_rawT line 225
  34. lemma OAI.Higman.RopeTrick.evaluate_relation line 233
  35. def OAI.Higman.RopeTrick.detect line 247
  36. lemma OAI.Higman.RopeTrick.detect_fMap line 253
  37. theorem OAI.Higman.RopeTrick.embeds_quotient line 261
  38. def OAI.Higman.IsBenign line 291
  39. lemma OAI.Higman.Double.firstIn_eq_secondIn line 297
  40. theorem OAI.Higman.embeds_of_benign_kernel line 303
  41. theorem OAI.Higman.IsBenign.of_fg line 326
  42. theorem OAI.Higman.IsBenign.inf line 330
  43. theorem OAI.Higman.IsBenign.comap line 342