OAI/GroupTheory/FiniteType/SteinbergFinitePresentation.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SteinbergFinitePresentation.Triple line 15
  2. abbrev OAI.SteinbergFinitePresentation.Quad line 16
  3. abbrev OAI.SteinbergFinitePresentation.Index line 18
  4. def OAI.SteinbergFinitePresentation.letter line 20
  5. def OAI.SteinbergFinitePresentation.relator line 23
  6. def OAI.SteinbergFinitePresentation.relations line 32
  7. abbrev OAI.SteinbergFinitePresentation.Universal line 33
  8. instance OAI.SteinbergFinitePresentation.(instance at line 35) line 35
  9. instance OAI.SteinbergFinitePresentation.(instance at line 42) line 42
  10. instance OAI.SteinbergFinitePresentation.(instance at line 44) line 44
  11. lemma OAI.SteinbergFinitePresentation.relator_eq_one line 46
  12. def OAI.SteinbergFinitePresentation.initial line 50
  13. abbrev OAI.SteinbergFinitePresentation.Coeff line 64
  14. def OAI.SteinbergFinitePresentation.coefficient line 65
  15. def OAI.SteinbergFinitePresentation.toSteinberg line 69
  16. lemma OAI.SteinbergFinitePresentation.toSteinberg_gen line 88
  17. def OAI.SteinbergFinitePresentation.fromSteinberg line 94
  18. lemma OAI.SteinbergFinitePresentation.polynomial_coefficient line 100
  19. lemma OAI.SteinbergFinitePresentation.from_to line 112
  20. lemma OAI.SteinbergFinitePresentation.toSteinberg_word line 119
  21. lemma OAI.SteinbergFinitePresentation.toSteinberg_polynomial line 135
  22. lemma OAI.SteinbergFinitePresentation.to_from line 148
  23. def OAI.SteinbergFinitePresentation.equiv line 155
  24. theorem OAI.SteinbergFinitePresentation.free_finitelyPresented line 164
  25. theorem OAI.SteinbergFinitePresentation.finitelyPresented line 170
  26. lemma OAI.SteinbergFinitePresentation.fin_six_outside line 180
  27. theorem OAI.SteinbergFinitePresentation.rank_six_finitelyPresented line 195
  28. abbrev OAI.HNNSubgroup.base line 210
  29. lemma OAI.HNNSubgroup.base_invariant line 213
  30. def OAI.HNNSubgroup.baseMap line 221
  31. lemma OAI.HNNSubgroup.baseMap_injective line 226
  32. def OAI.HNNSubgroup.inclusion line 230
  33. def OAI.HNNSubgroup.stableElement line 235
  34. lemma OAI.HNNSubgroup.inclusion_relation line 237
  35. def OAI.HNNSubgroup.hom line 242
  36. lemma OAI.HNNSubgroup.hom_injective line 246
  37. lemma OAI.HNNSubgroup.hom_surjective line 256
  38. def OAI.HNNSubgroup.equiv line 268