OAI/Topology/ArtinGroups/Functors/ZigzagLinear.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.zigzagLinear line 14
2. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.zigzag_vertex_core line 24
3. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.zigzag_vertex_leaf line 26
4. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.zigzag_arrow_core line 28
5. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.zigzag_arrow_leaf line 30
6. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.zigzag_token_core line 32
7. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.zigzag_token_leaf line 34
8. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.zigzagLinear_mul line 37
9. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.zigzag_vertexId line 64
10. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.zigzag_homogeneous line 75
11. def OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.placement line 92
12. def OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.matrix line 95
13. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.matrix_apply line 98
14. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.matrix_zero line 100
15. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.matrix_add line 102
16. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.matrix_mul line 105
17. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.matrix_entries line 111
18. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.matrix_degree line 124
19. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.matrix_identity line 133
20. def OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.complex line 144
21. lemma OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.complex_minimal line 151
22. def OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.chainMap line 158
23. def OAI.HarmonicArtin.ReversibleQuiver.ProbeEmbedding.homotopyEquivalence line 168