OAI/RingTheory/BassTrace/SparseChains.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.BarycentricChains.labelMap_natural_local line 17
  2. def OAI.BassTrace.Sparse.sparseChainFamily line 67
  3. lemma OAI.BassTrace.Sparse.sparseChainFamily_zero line 71
  4. lemma OAI.BassTrace.Sparse.sparseChainFamily_chain_face line 81
  5. def OAI.BassTrace.Sparse.augmentedComplex line 92
  6. lemma OAI.BassTrace.Sparse.sparseChainFamily_chain line 103
  7. lemma OAI.BassTrace.Sparse.sparseChainFamily_local_face line 119
  8. lemma OAI.BassTrace.Sparse.sparseChainFamily_local line 147
  9. lemma OAI.BassTrace.PathChains.tuple_connected line 192
  10. lemma OAI.BassTrace.PathChains.path_tuple_connected line 216
  11. def OAI.BassTrace.PathChains.topPaths line 234
  12. lemma OAI.BassTrace.PathChains.topPaths_mem line 238
  13. def OAI.BassTrace.PathChains.pathSupport line 244
  14. lemma OAI.BassTrace.PathChains.topPaths_card line 247
  15. lemma OAI.BassTrace.PathChains.pathSupport_pure line 252
  16. def OAI.BassTrace.PathChains.liftPath line 263
  17. lemma OAI.BassTrace.PathChains.liftPath_quotient line 266
  18. lemma OAI.BassTrace.PathChains.liftPath_mem line 275
  19. lemma OAI.BassTrace.PathChains.projection_path_relations line 303
  20. lemma OAI.BassTrace.PathChains.internal_path_cycle line 322