OAI/GroupTheory/FiniteType/AscendingTorus.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AscendingTorus.relation line 18
  2. abbrev OAI.AscendingTorus.relations line 21
  3. abbrev OAI.AscendingTorus.Torus line 24
  4. def OAI.AscendingTorus.of line 27
  5. def OAI.AscendingTorus.t line 30
  6. theorem OAI.AscendingTorus.of_mul_t line 33
  7. def OAI.AscendingTorus.lift line 48
  8. theorem OAI.AscendingTorus.lift_of line 58
  9. theorem OAI.AscendingTorus.lift_t line 63
  10. theorem OAI.AscendingTorus.hom_ext line 69
  11. theorem OAI.AscendingTorus.conj_of_image line 74
  12. def OAI.AscendingTorus.interleaveForward line 81
  13. def OAI.AscendingTorus.interleaveBase line 87
  14. theorem OAI.AscendingTorus.interleaveBase_apply line 90
  15. def OAI.AscendingTorus.interleaveBackward line 94
  16. theorem OAI.AscendingTorus.interleaveBackward_forward line 104
  17. theorem OAI.AscendingTorus.interleaveForward_backward line 116
  18. def OAI.AscendingTorus.interleaveEquiv line 128
  19. theorem OAI.AscendingTorus.map_relation_eq_one_iff line 136
  20. theorem OAI.AscendingTorus.normalClosure_relations_dense line 144
  21. theorem OAI.AscendingTorus.finitelyPresented line 166
  22. theorem OAI.AscendingTorus.finitelyPresented_of_factorization line 174
  23. def OAI.AscendingHNN.toPresentation line 186
  24. def OAI.AscendingHNN.fromPresentation line 189
  25. lemma OAI.AscendingHNN.toPresentation_embed line 192
  26. lemma OAI.AscendingHNN.toPresentation_stable line 194
  27. lemma OAI.AscendingHNN.fromPresentation_of line 196
  28. lemma OAI.AscendingHNN.fromPresentation_t line 198
  29. lemma OAI.AscendingHNN.from_to_presentation line 201
  30. lemma OAI.AscendingHNN.to_from_presentation line 206
  31. def OAI.AscendingHNN.presentationEquiv line 211
  32. theorem OAI.AscendingHNN.finitelyPresented_of_factorization line 220