OAI/Topology/ArtinGroups/Functors/Placement.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Iso.placement line 14
2. def OAI.HarmonicArtin.ReversibleQuiver.Iso.matrix line 17
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.matrix_apply line 20
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.matrix_zero line 23
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.matrix_add line 25
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.matrix_mul line 28
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.matrix_entries line 32
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.matrix_degree line 45
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.matrix_identity line 54
10. def OAI.HarmonicArtin.ReversibleQuiver.Iso.complex line 65
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.complex_minimal line 72
12. def OAI.HarmonicArtin.ReversibleQuiver.Iso.chainMap line 79
13. def OAI.HarmonicArtin.ReversibleQuiver.Iso.homotopyEquivalence line 89