OAI/RingTheory/BassTrace/AveragedChains.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.SubdivisionChains.originalHull_push line 26
  2. lemma OAI.BassTrace.SubdivisionChains.localFace_push line 33
  3. lemma OAI.BassTrace.SubdivisionChains.map_push_inverse line 44
  4. lemma OAI.BassTrace.SubdivisionChains.map_action_inverse line 52
  5. lemma OAI.BassTrace.SubdivisionChains.local_faces_natural line 60
  6. lemma OAI.BassTrace.SubdivisionChains.subdivision_natural_face line 81
  7. lemma OAI.BassTrace.Sparse.vertexMap_perm line 132
  8. lemma OAI.BassTrace.Sparse.sparseChainFamily_natural_face line 139
  9. lemma OAI.BassTrace.Sparse.sparseChainFamily_natural line 170
  10. def OAI.BassTrace.FiniteAverage.locallyConstantLinearMap line 215
  11. lemma OAI.BassTrace.FiniteAverage.locallyConstantLinearMap_post line 233
  12. lemma OAI.BassTrace.FiniteAverage.locallyConstantLinearMap_const line 239
  13. def OAI.BassTrace.Sparse.averagedSparseChain line 275
  14. lemma OAI.BassTrace.Sparse.averagedSparseChain_zero line 279
  15. lemma OAI.BassTrace.Sparse.averagedSparseChain_chain line 285
  16. lemma OAI.BassTrace.Sparse.averagedSparseChain_natural line 296
  17. lemma OAI.BassTrace.Sparse.averagedSparseChain_comparison line 315