OAI/Topology/ArtinGroups/Quivers/PathZero.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathZero line 10
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathOne line 27
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathZero_mul line 44
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathOne_mul line 60
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathZero_vertexId line 83
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathOne_vertexId line 84
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathZero_eq_zero line 86
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathOne_eq_self line 92
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.matrixZero line 101
10. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.matrixOne line 106
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.matrixZero_eq_zero line 111
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.matrixOne_eq_self line 117
13. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.matrixZero_mul line 123
14. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.matrixOne_mul line 132
15. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.matrixZero_entries line 143
16. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.matrixZero_degree line 156
17. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.matrixOne_homDifferential line 169
18. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.linear_boundary_primitive line 180