OAI/GroupTheory/UniversalGroup/AscendingTorus.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniversalFInfinity.AscendingTorus.Free line 23
  2. def OAI.UniversalFInfinity.AscendingTorus.letter line 25
  3. def OAI.UniversalFInfinity.AscendingTorus.relation line 27
  4. def OAI.UniversalFInfinity.AscendingTorus.relations line 30
  5. instance OAI.UniversalFInfinity.AscendingTorus.(instance at line 33) line 33
  6. def OAI.UniversalFInfinity.AscendingTorus.Torus line 36
  7. instance OAI.UniversalFInfinity.AscendingTorus.(instance at line 38) line 38
  8. instance OAI.UniversalFInfinity.AscendingTorus.groupOfHom line 42
  9. def OAI.UniversalFInfinity.AscendingTorus.of line 44
  10. def OAI.UniversalFInfinity.AscendingTorus.stable line 47
  11. lemma OAI.UniversalFInfinity.AscendingTorus.of_mul_stable line 50
  12. lemma OAI.UniversalFInfinity.AscendingTorus.stable_conjugate line 56
  13. lemma OAI.UniversalFInfinity.AscendingTorus.inverse_conjugate line 60
  14. def OAI.UniversalFInfinity.AscendingTorus.lift line 66
  15. lemma OAI.UniversalFInfinity.AscendingTorus.lift_of line 76
  16. lemma OAI.UniversalFInfinity.AscendingTorus.lift_stable line 82
  17. lemma OAI.UniversalFInfinity.AscendingTorus.hom_ext line 88
  18. theorem OAI.UniversalFInfinity.AscendingTorus.of_injective line 95
  19. def OAI.UniversalFInfinity.AscendingTorus.forward line 113
  20. def OAI.UniversalFInfinity.AscendingTorus.backward line 117
  21. lemma OAI.UniversalFInfinity.AscendingTorus.forward_of line 128
  22. lemma OAI.UniversalFInfinity.AscendingTorus.forward_stable line 132
  23. lemma OAI.UniversalFInfinity.AscendingTorus.backward_of line 135
  24. lemma OAI.UniversalFInfinity.AscendingTorus.backward_stable line 140
  25. lemma OAI.UniversalFInfinity.AscendingTorus.backward_forward line 143
  26. lemma OAI.UniversalFInfinity.AscendingTorus.forward_backward line 150
  27. def OAI.UniversalFInfinity.AscendingTorus.cyclicFactorization line 158
  28. lemma OAI.UniversalFInfinity.AscendingTorus.relations_finitelyNormallyGenerated line 166
  29. instance OAI.UniversalFInfinity.AscendingTorus.finitelyPresented line 212
  30. theorem OAI.UniversalFInfinity.AscendingTorus.finitelyPresented_of_factorization line 218
  31. lemma OAI.UniversalFInfinity.AscendingTorus.of_mul_stable_pow line 231
  32. lemma OAI.UniversalFInfinity.AscendingTorus.inv_stable_pow_mul_of line 240
  33. def OAI.UniversalFInfinity.AscendingTorus.normalForms line 246
  34. lemma OAI.UniversalFInfinity.AscendingTorus.of_mem_normalForms line 271
  35. lemma OAI.UniversalFInfinity.AscendingTorus.stable_mem_normalForms line 274
  36. theorem OAI.UniversalFInfinity.AscendingTorus.normal_form line 277
  37. def OAI.UniversalFInfinity.AscendingTorus.height line 295
  38. lemma OAI.UniversalFInfinity.AscendingTorus.height_of line 298
  39. lemma OAI.UniversalFInfinity.AscendingTorus.height_stable line 301
  40. abbrev OAI.UniversalFInfinity.AscendingTorus.Coset line 311
  41. def OAI.UniversalFInfinity.AscendingTorus.coset line 313
  42. lemma OAI.UniversalFInfinity.AscendingTorus.coset_mul_of line 315
  43. def OAI.UniversalFInfinity.AscendingTorus.next line 319
  44. lemma OAI.UniversalFInfinity.AscendingTorus.next_coset line 328
  45. lemma OAI.UniversalFInfinity.AscendingTorus.next_iterate_coset line 331
  46. lemma OAI.UniversalFInfinity.AscendingTorus.reaches_base_ray line 338
  47. lemma OAI.UniversalFInfinity.AscendingTorus.common_descendant line 347
  48. def OAI.UniversalFInfinity.AscendingTorus.cosetHeight line 355
  49. lemma OAI.UniversalFInfinity.AscendingTorus.cosetHeight_coset line 363
  50. lemma OAI.UniversalFInfinity.AscendingTorus.height_next line 366
  51. def OAI.UniversalFInfinity.AscendingTorus.origin line 374
  52. lemma OAI.UniversalFInfinity.AscendingTorus.coset_origin line 376
  53. lemma OAI.UniversalFInfinity.AscendingTorus.origin_next_mem line 379
  54. def OAI.UniversalFInfinity.AscendingTorus.cosetOffset line 385
  55. lemma OAI.UniversalFInfinity.AscendingTorus.origin_next line 388
  56. lemma OAI.UniversalFInfinity.AscendingTorus.smul_coset line 400
  57. lemma OAI.UniversalFInfinity.AscendingTorus.next_smul line 401
  58. lemma OAI.UniversalFInfinity.AscendingTorus.origin_action_mem line 405
  59. def OAI.UniversalFInfinity.AscendingTorus.actionOffset line 411
  60. lemma OAI.UniversalFInfinity.AscendingTorus.origin_action line 413
  61. lemma OAI.UniversalFInfinity.AscendingTorus.actionOffset_one line 419
  62. lemma OAI.UniversalFInfinity.AscendingTorus.actionOffset_mul line 424
  63. lemma OAI.UniversalFInfinity.AscendingTorus.actionOffset_next line 430