OAI/GroupTheory/FiniteType/AscendingHNNInnerTwist.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AscendingHNN.innerTwist line 11
  2. lemma OAI.AscendingHNN.innerTwist_apply line 13
  3. lemma OAI.AscendingHNN.innerTwist_injective line 16
  4. lemma OAI.AscendingHNN.changed_stable_relation line 19
  5. def OAI.AscendingHNN.changeStableHom line 26
  6. lemma OAI.AscendingHNN.restored_stable_relation line 30
  7. def OAI.AscendingHNN.restoreStableHom line 41
  8. lemma OAI.AscendingHNN.changeStableHom_embed line 47
  9. lemma OAI.AscendingHNN.changeStableHom_stable line 51
  10. lemma OAI.AscendingHNN.restoreStableHom_embed line 55
  11. lemma OAI.AscendingHNN.restoreStableHom_stable line 59
  12. lemma OAI.AscendingHNN.change_restore line 64
  13. lemma OAI.AscendingHNN.restore_change line 70
  14. def OAI.AscendingHNN.changeStableEquiv line 76
  15. def OAI.HomStabilizer.fixedTuple line 88
  16. lemma OAI.HomStabilizer.mem_fixedTuple line 97
  17. def OAI.HomStabilizer.preimageEquiv line 100
  18. def OAI.TorusStabilizer.stageSubgroup line 116
  19. def OAI.TorusStabilizer.limitSubgroup line 118
  20. def OAI.TorusStabilizer.changedSubgroup line 121
  21. lemma OAI.TorusStabilizer.changed_stable_mem line 125
  22. lemma OAI.TorusStabilizer.base_mem_iff line 139
  23. def OAI.TorusStabilizer.torusEquiv line 150
  24. structure OAI.StageGeometry.PairDiagrams line 165
  25. abbrev OAI.StageGeometry.trans line 187
  26. abbrev OAI.StageGeometry.transInjective line 188
  27. abbrev OAI.StageGeometry.shift line 189
  28. lemma OAI.StageGeometry.compatible line 191
  29. abbrev OAI.StageGeometry.changed line 198
  30. abbrev OAI.StageGeometry.base line 201
  31. abbrev OAI.StageGeometry.endomorphism line 205
  32. abbrev OAI.StageGeometry.endomorphism_injective line 210
  33. lemma OAI.StageGeometry.base_iff line 218
  34. lemma OAI.StageGeometry.compressed_tuple line 223
  35. def OAI.StageGeometry.baseEquiv line 226
  36. abbrev OAI.StageGeometry.compressedUnits line 242
  37. lemma OAI.StageGeometry.compressed_fixed line 246
  38. lemma OAI.StageGeometry.compressed_point_fixed line 253
  39. lemma OAI.StageGeometry.units_prefix line 258
  40. lemma OAI.StageGeometry.units_suffix line 265
  41. abbrev OAI.StageGeometry.conjugated line 275
  42. lemma OAI.StageGeometry.conjugated_mem line 279
  43. def OAI.StageGeometry.diagramMap line 302
  44. def OAI.StageGeometry.splittings line 309
  45. theorem OAI.StageGeometry.factor line 337
  46. theorem OAI.StageGeometry.aligned_geometric line 359
  47. theorem OAI.StageGeometry.aligned_geometric_of_ring_presentation line 380