OAI/Topology/ArtinGroups/Quivers/VertexLinear.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertexLinear line 11
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.arrowLinear line 16
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertex_sum line 21
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.arrow_sum line 25
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.TokenMatrix line 29
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.matrixTwo_eq_self line 32
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.tokenMatrix_sub line 38
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.tokenMatrix_smul line 47
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.tokenMatrix_matrixTwo_mul line 56
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.tokenMatrix_mul_matrixTwo line 74
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.tokenHomDifferential_tokenMatrix line 95
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homDifferential_tokenMatrix line 103