OAI/Topology/ArtinGroups/Complexes/TokenShift.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.tokenShift line 14
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.testShiftIndexEquiv line 30
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.normalizedTestTwist line 56
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.normalizedTestTwist_pivot_entry line 60
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.testShiftPivot line 81
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.normalizedTestTwist_unit_token line 100
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.normalizedTestTwist_token_token line 111
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.testShift_reduced_eq line 126
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveTwist_testShift line 138