OAI/Topology/ArtinGroups/Functors/ReversibleQuiverMap.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.complex_symm line 18
2. def OAI.HarmonicArtin.ReversibleQuiver.Iso.classMap line 38
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.classMap_complex line 44
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.classMap_symm line 48
5. def OAI.HarmonicArtin.ReversibleQuiver.Iso.classEquiv line 53
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.classMap_positiveTwist line 59
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.loopless line 69
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.orthogonal line 76
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.orthogonal_pairwise line 87
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.classMap_packet line 92
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Iso.classMap_packet_inverse line 125