OAI/Algebra/GroupRing/AbsorbTracks.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TorsionFreeZeroDivisors.AbsorbTracks.graph line 22
  2. def OAI.TorsionFreeZeroDivisors.AbsorbTracks.initial line 23
  3. lemma OAI.TorsionFreeZeroDivisors.AbsorbTracks.initial_vertex line 24
  4. def OAI.TorsionFreeZeroDivisors.AbsorbTracks.boundaryLoop line 26
  5. def OAI.TorsionFreeZeroDivisors.AbsorbTracks.initialTrack line 27
  6. def OAI.TorsionFreeZeroDivisors.AbsorbTracks.cellMap line 30
  7. lemma OAI.TorsionFreeZeroDivisors.AbsorbTracks.cellMap_boundary line 33
  8. def OAI.TorsionFreeZeroDivisors.AbsorbTracks.physical line 39
  9. abbrev OAI.TorsionFreeZeroDivisors.AbsorbTracks.Coef line 44
  10. def OAI.TorsionFreeZeroDivisors.AbsorbTracks.obstruction line 45
  11. def OAI.TorsionFreeZeroDivisors.AbsorbTracks.obstructionMap line 47
  12. lemma OAI.TorsionFreeZeroDivisors.AbsorbTracks.obstructionMap_single line 49
  13. def OAI.TorsionFreeZeroDivisors.AbsorbTracks.turnBack line 51
  14. def OAI.TorsionFreeZeroDivisors.AbsorbTracks.correction line 55
  15. def OAI.TorsionFreeZeroDivisors.AbsorbTracks.labels line 56
  16. lemma OAI.TorsionFreeZeroDivisors.AbsorbTracks.labels_vertex line 58
  17. def OAI.TorsionFreeZeroDivisors.AbsorbTracks.final line 61
  18. lemma OAI.TorsionFreeZeroDivisors.AbsorbTracks.final_vertex line 63
  19. def OAI.TorsionFreeZeroDivisors.AbsorbTracks.finalTrack line 67
  20. lemma OAI.TorsionFreeZeroDivisors.AbsorbTracks.response line 71
  21. lemma OAI.TorsionFreeZeroDivisors.AbsorbTracks.homotopic line 93