OAI/RingTheory/BassTrace/PathComplex.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BassTrace.PathChains.relations line 20
  2. abbrev OAI.BassTrace.PathChains.Coinvariant line 24
  3. def OAI.BassTrace.PathChains.quotientMap line 26
  4. lemma OAI.BassTrace.PathChains.quotientMap_invariant line 29
  5. lemma OAI.BassTrace.PathChains.d_relations line 36
  6. def OAI.BassTrace.PathChains.quotientD line 49
  7. lemma OAI.BassTrace.PathChains.quotientD_mk line 55
  8. def OAI.BassTrace.PathChains.pathProjection line 58
  9. lemma OAI.BassTrace.PathChains.pathProjection_mk line 67
  10. lemma OAI.BassTrace.PathChains.projected_twist line 71
  11. lemma OAI.BassTrace.PathChains.pathProjection_twist line 80
  12. def OAI.BassTrace.PathChains.pathChain line 89
  13. lemma OAI.BassTrace.PathChains.pathChain_twist line 93
  14. lemma OAI.BassTrace.PathChains.pathChain_odd line 110
  15. lemma OAI.BassTrace.PathChains.pathProjection_boundary line 127
  16. lemma OAI.BassTrace.PathChains.pathChain_boundary line 138
  17. theorem OAI.BassTrace.PathChains.pathChain_even_cycle line 157
  18. def OAI.BassTrace.PathChains.quotientCocycle line 167
  19. lemma OAI.BassTrace.PathChains.quotientCocycle_pathProjection line 179
  20. lemma OAI.BassTrace.PathChains.quotientCocycle_pairing line 184
  21. lemma OAI.BassTrace.PathChains.quotientCocycle_closed line 193