OAI/GroupTheory/FiniteType/ClassifyingSpaces.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SimpleFInftyOvergroups.HasTypeFInfty.of_equiv line 10
  2. theorem OAI.SimpleFInftyOvergroups.ascending_hnn_geometric line 15
  3. theorem OAI.SimpleFInftyOvergroups.ascending_torus_geometric line 35
  4. abbrev OAI.FiniteExtension.Q line 50
  5. def OAI.FiniteExtension.pi line 51
  6. def OAI.FiniteExtension.sectionMap line 53
  7. lemma OAI.FiniteExtension.section_one line 56
  8. lemma OAI.FiniteExtension.pi_section line 57
  9. lemma OAI.FiniteExtension.pi_coe line 61
  10. def OAI.FiniteExtension.factor line 64
  11. def OAI.FiniteExtension.twist line 68
  12. def OAI.FiniteExtension.cocycle line 71
  13. lemma OAI.FiniteExtension.factor_one line 72
  14. lemma OAI.FiniteExtension.factor_coe line 73
  15. lemma OAI.FiniteExtension.factor_section line 74
  16. lemma OAI.FiniteExtension.twist_coe line 76
  17. lemma OAI.FiniteExtension.cocycle_coe line 78
  18. lemma OAI.FiniteExtension.factor_mul line 81
  19. abbrev OAI.FiniteExtension.Pre line 87
  20. def OAI.FiniteExtension.inK line 88
  21. def OAI.FiniteExtension.letter line 89
  22. def OAI.FiniteExtension.mulRel line 90
  23. def OAI.FiniteExtension.conjRel line 92
  24. def OAI.FiniteExtension.rels line 95
  25. abbrev OAI.FiniteExtension.N line 98
  26. abbrev OAI.FiniteExtension.Presented line 99
  27. def OAI.FiniteExtension.quot line 100
  28. def OAI.FiniteExtension.incl line 101
  29. def OAI.FiniteExtension.t line 102
  30. lemma OAI.FiniteExtension.rel_eq_one line 104
  31. lemma OAI.FiniteExtension.t_one line 106
  32. lemma OAI.FiniteExtension.t_mul line 108
  33. lemma OAI.FiniteExtension.t_conj_gen line 112
  34. lemma OAI.FiniteExtension.t_conj line 116
  35. def OAI.FiniteExtension.retract line 128
  36. lemma OAI.FiniteExtension.retract_coe line 140
  37. lemma OAI.FiniteExtension.retract_section line 142
  38. def OAI.FiniteExtension.evaluatePre line 145
  39. lemma OAI.FiniteExtension.evaluatePre_inK line 146
  40. lemma OAI.FiniteExtension.evaluatePre_letter line 148
  41. lemma OAI.FiniteExtension.rels_ker line 150
  42. def OAI.FiniteExtension.evaluate line 164
  43. lemma OAI.FiniteExtension.evaluate_quot line 166
  44. lemma OAI.FiniteExtension.evaluate_incl line 168
  45. lemma OAI.FiniteExtension.evaluate_t line 171
  46. lemma OAI.FiniteExtension.evaluate_retract line 175
  47. lemma OAI.FiniteExtension.retract_evaluate line 177
  48. def OAI.FiniteExtension.presentationEquiv line 192
  49. lemma OAI.FiniteExtension.rels_finite line 198
  50. theorem OAI.FiniteExtension.finitelyPresented line 202