OAI/RingTheory/BassTrace/AdmissibleCuts.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BassTrace.Sparse.GraphGeometry.onFinsupp_faces_countable line 37
2. theorem OAI.BassTrace.Sparse.GraphGeometry.admissibleStep_of_center_cover line 44
3. theorem OAI.BassTrace.Sparse.GraphGeometry.exists_admissibleStep line 134
4. structure OAI.BassTrace.Sparse.OrbitForms.MarkedPair line 160
5. structure OAI.BassTrace.Sparse.OrbitForms.SeparatingFiltration line 166
6. def OAI.BassTrace.Sparse.OrbitForms.SeparatingFiltration.point line 180
7. lemma OAI.BassTrace.Sparse.GraphGeometry.onFinsupp_faces_push line 209
8. def OAI.BassTrace.Sparse.GraphGeometry.originalMarkedPair line 220
9. theorem OAI.BassTrace.Sparse.GraphGeometry.exists_separatingFiltration line 249