OAI/Topology/ArtinGroups/Complexes/DiagonalVertex.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.tokenBasis_mul_positive line 13
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.positive_mul_tokenBasis line 33
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace_tokenBasis line 53
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homBoundary_positive line 61
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.diagonalVertex line 74
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.diagonalVertex_boundary line 81
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.identity_mem_homCycles line 89
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.diagonalVertex_identity line 94
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.diagonalToken line 99
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.diagonalToken_entries line 102
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.diagonalToken_degree line 128
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.diagonalToken_mem_homCycles line 146
13. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.supertrace_diagonalToken line 169