OAI/GroupTheory/FiniteType/AscendingHNN.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AscendingHNN.associatedEquiv line 15
  2. abbrev OAI.AscendingHNN.Torus line 18
  3. def OAI.AscendingHNN.embed line 20
  4. def OAI.AscendingHNN.stable line 22
  5. lemma OAI.AscendingHNN.embed_injective line 24
  6. lemma OAI.AscendingHNN.embed_mul_stable line 26
  7. lemma OAI.AscendingHNN.embed_mul_stable_pow line 30
  8. lemma OAI.AscendingHNN.expand_normal line 39
  9. theorem OAI.AscendingHNN.normal_form line 48
  10. def OAI.AscendingHNN.heightHom line 67
  11. def OAI.AscendingHNN.height line 70
  12. lemma OAI.AscendingHNN.height_mul line 72
  13. lemma OAI.AscendingHNN.height_embed line 76
  14. lemma OAI.AscendingHNN.height_stable line 79
  15. lemma OAI.AscendingHNN.height_inv line 82
  16. abbrev OAI.AscendingHNN.Vertex line 85
  17. def OAI.AscendingHNN.parent line 87
  18. lemma OAI.AscendingHNN.parent_mk line 99
  19. lemma OAI.AscendingHNN.parent_iterate_mk line 102
  20. def OAI.AscendingHNN.vertexHeight line 109
  21. lemma OAI.AscendingHNN.vertexHeight_mk line 117
  22. lemma OAI.AscendingHNN.parent_raises line 120
  23. lemma OAI.AscendingHNN.forward_meets_base line 125
  24. lemma OAI.AscendingHNN.forward_merge line 138
  25. lemma OAI.AscendingHNN.parent_smul line 151
  26. abbrev OAI.AscendingHNN.treeComplex line 159
  27. theorem OAI.AscendingHNN.treeComplex_shortExact line 162
  28. def OAI.ListChains.IdempotentSplittings.conjugate line 173
  29. lemma OAI.ListChains.uniformFillings_conjugate_of_factorization line 184
  30. abbrev OAI.AscendingHNN.baseEquiv line 208
  31. abbrev OAI.AscendingHNN.baseShift line 211
  32. lemma OAI.AscendingHNN.baseShift_relation line 215
  33. theorem OAI.AscendingHNN.regular_product_homology_vanishes line 226
  34. lemma OAI.AscendingHNN.hom_ext line 243
  35. lemma OAI.AscendingHNN.inv_conjugation line 255
  36. def OAI.AscendingHNN.evaluation line 260
  37. lemma OAI.AscendingHNN.evaluation_embed line 263
  38. lemma OAI.AscendingHNN.evaluation_stable line 266
  39. lemma OAI.AscendingHNN.evaluation_normal line 272
  40. lemma OAI.AscendingHNN.evaluation_injective line 277
  41. lemma OAI.AscendingHNN.evaluation_surjective line 298