OAI/Topology/ArtinGroups/Quivers/PathTwo.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathTwo line 11
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.path_decomposition line 28
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.pathTwo_mul_positive line 38
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.positive_mul_pathTwo line 41
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.matrixTwo line 46
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.matrix_decomposition line 51
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.positive_matrix_decomposition line 57
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.matrixTwo_mul_positive line 63
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.positive_mul_matrixTwo line 71
10. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.linearHomDifferential line 82
11. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.tokenHomDifferential line 94
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.tokenHomDifferential_apply line 99
13. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.tokenHomDifferential_positive line 112
14. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homDifferential_eq_linear_add_token line 119
15. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.secondary_kernel_zero line 127