OAI/Topology/ArtinGroups/Complexes/ArrowShift.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.arrowShift line 12
2. abbrev OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.AdjacentTestIndex line 25
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.adjacentTestIndexEquiv line 29
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.normalizedAdjacentTest line 65
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.adjacentTest_first_pivot_entry line 70
6. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.adjacentTestFirstPivot line 77
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.adjacentTest_first_source_retained line 91
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.adjacentTest_first_reduced_entry line 103
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.adjacentTest_second_pivot_entry line 112
10. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.adjacentTestSecondPivot line 133
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.adjacentTest_retained_to_second_target line 152
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.adjacentTest_retained_entry line 162
13. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.adjacentTest_second_reduced_differential line 175
14. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.adjacentTestReduction line 184