OAI/RingTheory/BassTrace/BarycentricChains.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.ChainHomotopy.tuple_image_perm line 17
  2. def OAI.BassTrace.ChainHomotopy.Complex.projectionValues line 25
  3. def OAI.BassTrace.ChainHomotopy.Complex.projection line 43
  4. lemma OAI.BassTrace.ChainHomotopy.Complex.projection_wedge line 48
  5. lemma OAI.BassTrace.ChainHomotopy.Complex.projection_self line 56
  6. lemma OAI.BassTrace.ChainHomotopy.Complex.chains_zero line 67
  7. lemma OAI.BassTrace.ChainHomotopy.Complex.image_mem_iff line 77
  8. lemma OAI.BassTrace.ChainHomotopy.Complex.projection_relabel line 85
  9. lemma OAI.BassTrace.ChainHomotopy.source_coinvariant_comparison line 106
  10. def OAI.BassTrace.BarycentricChains.stepValues line 158
  11. def OAI.BassTrace.BarycentricChains.labelMap line 167
  12. lemma OAI.BassTrace.BarycentricChains.labelMap_wedge_succ line 171
  13. lemma OAI.BassTrace.BarycentricChains.labelMap_wedge_zero line 177
  14. lemma OAI.BassTrace.BarycentricChains.labelMap_wedge_recursion line 183
  15. lemma OAI.BassTrace.BarycentricChains.boundary_degree_zero line 191
  16. lemma OAI.BassTrace.BarycentricChains.labelMap_chain line 199
  17. lemma OAI.BassTrace.BarycentricChains.labelMap_natural line 224
  18. lemma OAI.BassTrace.BarycentricChains.labelMap_local line 251