OAI/Topology/ArtinGroups/Quivers/Path.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.ReversibleQuiver.Path line 8
2. def OAI.HarmonicArtin.ReversibleQuiver.Path.source line 14
3. def OAI.HarmonicArtin.ReversibleQuiver.Path.target line 19
4. def OAI.HarmonicArtin.ReversibleQuiver.Path.length line 24
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathCoordinates line 38
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathCoordinates_vertex line 47
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathCoordinates_arrow line 49
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathCoordinates_token line 51
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathBasis line 56
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathBasis_repr line 60
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathBasis_coordinates line 63
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.sum_pathBasis line 68
13. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathBasis_vertex line 71
14. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathBasis_arrow line 79
15. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathBasis_token line 87
16. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.coordinates_vertexId_left line 96
17. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.coordinates_vertexId_right line 108
18. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathBasis_left line 119
19. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathBasis_right line 129
20. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.coordinates_homogeneous line 140
21. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathBasis_homogeneous line 161
22. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.coordinates_corner line 170
23. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.coordinates_mul_degree line 185