OAI/RingTheory/BassTrace/EquivariantSurgery.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BassTrace.Sparse.OrbitForms.EquivariantStep line 20
2. def OAI.BassTrace.Sparse.OrbitForms.EquivariantStep.result line 25
3. def OAI.BassTrace.Sparse.OrbitForms.SeparatingFiltration.NearMinimal line 32
4. theorem OAI.BassTrace.Sparse.OrbitForms.exists_nearMinimal_filtration line 40
5. theorem OAI.BassTrace.Sparse.GraphGeometry.exists_normalized_nearMinimal line 113
6. lemma OAI.BassTrace.Sparse.OrbitForms.step_dimension_bound line 149
7. lemma OAI.BassTrace.Sparse.OrbitForms.normalizedArea_step_lt_top line 166
8. lemma OAI.BassTrace.Sparse.Cuts.Subdivision.marked_complement_of_patch line 191
9. lemma OAI.BassTrace.Sparse.Cuts.replacement_componentDiameter line 213
10. lemma OAI.BassTrace.Sparse.Cuts.DimensionDrop.union_levels line 261
11. def OAI.BassTrace.Sparse.Cuts.UniversalCuts.replacementStep line 294
12. lemma OAI.BassTrace.Sparse.BallOrbitForms.outerPatch_mem line 402