OAI/RingTheory/BassTrace/SparseBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BassTrace.Sparse.sparseChainFamily_bound line 39
2. lemma OAI.BassTrace.Sparse.averagedSparseChain_bound line 116
3. lemma OAI.BassTrace.BarycentricChains.finite_norm_bound line 148
4. lemma OAI.BassTrace.BarycentricChains.exists_finite_wedge_bound line 155
5. lemma OAI.BassTrace.Sparse.exists_chain_bound line 193
6. lemma OAI.BassTrace.Sparse.vanishing_of_zero_strata line 244
7. lemma OAI.BassTrace.Sparse.GraphGeometry.augmentedComplex_invariant line 316
8. theorem OAI.BassTrace.Sparse.GraphGeometry.sparse_vanishing line 327
9. lemma OAI.BassTrace.Sparse.GraphGeometry.graphMetric_action_isometry line 348