OAI/RingTheory/BassTrace/DirectedCuts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BassTrace.Sparse.Cuts.exists_finite_coordinate_patch line 16
  2. def OAI.BassTrace.Sparse.Cuts.complexParents line 34
  3. lemma OAI.BassTrace.Sparse.Cuts.mem_complexParents line 37
  4. lemma OAI.BassTrace.Sparse.Cuts.complexParents_affineImage line 42
  5. lemma OAI.BassTrace.Sparse.Cuts.complexParents_space line 60
  6. theorem OAI.BassTrace.Sparse.Cuts.exists_canonical_simplicialCuts line 71
  7. def OAI.BassTrace.Sparse.Cuts.directedUnionComplex line 122
  8. lemma OAI.BassTrace.Sparse.Cuts.directedUnionComplex_space line 137
  9. def OAI.BassTrace.Sparse.Cuts.finitePatch line 144
  10. lemma OAI.BassTrace.Sparse.Cuts.finitePatch_finite line 158
  11. lemma OAI.BassTrace.Sparse.Cuts.finitePatch_mono line 166
  12. lemma OAI.BassTrace.Sparse.Cuts.mem_finitePatch line 172