OAI/Topology/ArtinGroups/Quivers/VertexHom.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertexHom line 12
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertexId line 19
3. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertex_vertexId line 22
4. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.arrow_vertexId line 25
5. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.token_vertexId line 28
6. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertexId_mul_self line 31
7. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.PositiveMatrix line 43
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.positiveMatrix_add line 47
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.positiveMatrix_mul_left line 54
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.positiveMatrix_mul_right line 67
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.positiveMatrix_triple line 81