OAI/GroupTheory/UniversalGroup/PathExtensions.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalFInfinity.PathExtension.Q.trans_cast line 19
  2. lemma OAI.UniversalFInfinity.PathExtension.Q.map_trans line 23
  3. lemma OAI.UniversalFInfinity.PathExtension.Q.map_refl line 29
  4. lemma OAI.UniversalFInfinity.PathExtension.Q.map_symm line 31
  5. structure OAI.UniversalFInfinity.PathExtension.Q.Equal line 36
  6. lemma OAI.UniversalFInfinity.PathExtension.Q.Equal.refl line 43
  7. lemma OAI.UniversalFInfinity.PathExtension.Q.Equal.ofEq line 44
  8. lemma OAI.UniversalFInfinity.PathExtension.Q.Equal.symm line 45
  9. lemma OAI.UniversalFInfinity.PathExtension.Q.Equal.trans line 48
  10. lemma OAI.UniversalFInfinity.PathExtension.Q.Equal.map line 52
  11. lemma OAI.UniversalFInfinity.PathExtension.Q.Equal.comp line 59
  12. lemma OAI.UniversalFInfinity.PathExtension.Q.cast_equal line 69
  13. lemma OAI.UniversalFInfinity.PathExtension.Q.refl_equal line 71
  14. def OAI.UniversalFInfinity.PathExtension.smulMap line 80
  15. lemma OAI.UniversalFInfinity.PathExtension.map_one_equal line 82
  16. lemma OAI.UniversalFInfinity.PathExtension.map_mul_equal line 88
  17. abbrev OAI.UniversalFInfinity.PathExtension.Extension line 95
  18. lemma OAI.UniversalFInfinity.PathExtension.ext line 99
  19. instance OAI.UniversalFInfinity.PathExtension.(instance at line 102) line 102
  20. instance OAI.UniversalFInfinity.PathExtension.(instance at line 104) line 104
  21. instance OAI.UniversalFInfinity.PathExtension.(instance at line 106) line 106
  22. lemma OAI.UniversalFInfinity.PathExtension.mul_path_equal line 109
  23. lemma OAI.UniversalFInfinity.PathExtension.one_path_equal line 114
  24. lemma OAI.UniversalFInfinity.PathExtension.mul_assoc line 118
  25. lemma OAI.UniversalFInfinity.PathExtension.one_mul line 129
  26. lemma OAI.UniversalFInfinity.PathExtension.mul_one line 136
  27. lemma OAI.UniversalFInfinity.PathExtension.inv_mul_cancel line 144
  28. instance OAI.UniversalFInfinity.PathExtension.(instance at line 153) line 153
  29. def OAI.UniversalFInfinity.PathExtension.projection line 159
  30. lemma OAI.UniversalFInfinity.PathExtension.natural_smul_equal line 173
  31. def OAI.UniversalFInfinity.PathExtension.mapFun line 180
  32. lemma OAI.UniversalFInfinity.PathExtension.mapFun_equal line 183
  33. lemma OAI.UniversalFInfinity.PathExtension.mapFun_one line 186
  34. lemma OAI.UniversalFInfinity.PathExtension.mapFun_mul line 193
  35. def OAI.UniversalFInfinity.PathExtension.map line 204
  36. lemma OAI.UniversalFInfinity.PathExtension.projection_map line 209
  37. lemma OAI.UniversalFInfinity.Cayley.smul_vertex line 220
  38. def OAI.UniversalFInfinity.Cayley.pathGenerator line 222
  39. def OAI.UniversalFInfinity.Cayley.wordLift line 225
  40. lemma OAI.UniversalFInfinity.Cayley.projection_wordLift line 227
  41. lemma OAI.UniversalFInfinity.Cayley.wordLift_fst line 231
  42. def OAI.UniversalFInfinity.Cayley.relatorClass line 235
  43. def OAI.UniversalFInfinity.Cayley.relatorLoop line 237
  44. lemma OAI.UniversalFInfinity.Cayley.relatorLoop_eq line 239
  45. lemma OAI.UniversalFInfinity.Cayley.relatorLoop_equal line 242
  46. def OAI.UniversalFInfinity.Cayley.relatorAttaching line 247
  47. abbrev OAI.UniversalFInfinity.Cayley.PresentationCover line 248
  48. def OAI.UniversalFInfinity.Cayley.presentationBase line 249
  49. lemma OAI.UniversalFInfinity.Cayley.presentationBase_smul line 250
  50. def OAI.UniversalFInfinity.Cayley.coverWordLift line 253
  51. lemma OAI.UniversalFInfinity.Cayley.mapped_relator_homotopic line 257
  52. lemma OAI.UniversalFInfinity.Cayley.coverWordLift_relator line 270
  53. lemma OAI.UniversalFInfinity.Cayley.coverWordLift_ker line 280
  54. def OAI.UniversalFInfinity.Cayley.presentationSection line 287
  55. lemma OAI.UniversalFInfinity.Cayley.presentationSection_lift line 291
  56. lemma OAI.UniversalFInfinity.Cayley.presentationSection_fst line 295
  57. lemma OAI.UniversalFInfinity.Cayley.vertex_action line 312
  58. lemma OAI.UniversalFInfinity.Cayley.pathGenerator_equal line 315
  59. lemma OAI.UniversalFInfinity.Cayley.edge_smul_equal line 321
  60. def OAI.UniversalFInfinity.Cayley.coherentClass line 336
  61. def OAI.UniversalFInfinity.Cayley.coherentPath line 338
  62. lemma OAI.UniversalFInfinity.Cayley.coherentPath_equal line 340
  63. lemma OAI.UniversalFInfinity.Cayley.coherentPath_edge line 346
  64. def OAI.UniversalFInfinity.Cayley.nullhomotopyOfSection line 366
  65. lemma OAI.UniversalFInfinity.Cayley.presentationSection_generator line 377
  66. def OAI.UniversalFInfinity.Cayley.presentationGraphNullhomotopy line 389
  67. lemma OAI.UniversalFInfinity.Attachment.exists_equivariant_extension line 404
  68. lemma OAI.UniversalFInfinity.Attachment.compactFundamentalSet line 422