OAI/Topology/ArtinGroups/Complexes/InverseTwistPlacement.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistPlacement line 12
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.normalizedInverseTwist_placement line 24
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistProjection line 41
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistInjection line 47
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistHomotopy line 53
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistProjection_entries line 60
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistProjection_degree line 79
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistInjection_entries line 90
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistInjection_degree line 109
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistHomotopy_entries line 122
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistHomotopy_degree line 145