OAI/Topology/ArtinGroups/Complexes/PositiveTwistHomotopy.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveTwistHomotopy line 15
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeTwistHomotopy line 19
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveTwistHomotopy_entries line 23
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeTwistHomotopy_entries line 44
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveTwistHomotopy_degree line 65
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeTwistHomotopy_degree line 85
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveTwistHomotopy_boundary line 105
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeTwistHomotopy_boundary line 123
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveTwist_identity line 140
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeTwist_identity line 151
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveTwist_homotopy_equation line 162
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeTwist_homotopy_equation line 180
13. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomotopyEquivalence.positiveTwist line 202
14. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomotopyEquivalence.negativeTwist line 218