OAI/Topology/ArtinGroups/Quivers/OrthogonalVertices.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.OrthogonalVertices line 10
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.OrthogonalVertices.symm line 13
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.no_corner_of_orthogonal line 20
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ext_placement_differential line 33
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomotopyEquivalence.symm line 44
6. abbrev OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.CommuteTwistIndex line 58
7. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.commuteTwistIndexEquiv line 61
8. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.normalizedCommuteTwist line 80
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.commuteTwistPlacement line 85
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.normalizedCommuteTwist_placement line 94
11. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.commuteTwistDifferential line 100
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.normalizedCommuteTwist_differential line 110