OAI/Topology/ArtinGroups/Quivers/SmulMul.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.smul_mul line 11
2. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mul_smul line 31
3. instance OAI.HarmonicArtin.ReversibleQuiver.Zigzag.(instance at line 51) line 51
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.homogeneous_zero line 54
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.homogeneous_add line 57
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.homogeneous_neg line 65
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.homogeneous_sum line 71
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.homogeneous_mul line 82
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.projectiveEntries_zero line 104
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.projectiveEntries_add line 108
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.projectiveEntries_neg line 121
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.projectiveEntries_mul line 133
13. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.projectiveEntries_identity line 143
14. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.projectiveIdentity_mul line 148
15. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mul_projectiveIdentity line 156
16. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mapDegree_zero line 164
17. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mapDegree_add line 168
18. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mapDegree_neg line 175
19. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mapDegree_mul line 180
20. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.homogeneous_vertexId line 201
21. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mapDegree_identity line 204