OAI/Topology/ArtinGroups/Complexes/CochainSignSubOne.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cochainSign_sub_one line 18
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cochainSign_sub_two line 23
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.signedCorner_sum line 27
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.signedGeneratorVector_mulVec line 49
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.signedGeneratorVector_test line 59
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.placementSignedWeight_lower line 82
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.signedGeneratorVector_cone line 89
8. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.signedGeneratorVector_positiveTwist line 97
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classSignedVector_positiveTwist line 110
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.placementSignedWeight_raise line 117
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.signedGeneratorVector_cocone line 124
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.signedGeneratorVector_cotest line 132
13. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.signedGeneratorVector_negativeTwist line 144
14. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classSignedVector_negativeTwist line 157
15. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classSignedVector_positiveWord line 163