OAI/Topology/ArtinGroups/Functors/LeftPacketIndex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.LeftPacketIndex line 21
2. abbrev OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.RightPacketIndex line 23
3. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.leftPacketEquiv line 26
4. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.rightPacketEquiv line 34
5. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearMap_scalarVertex line 42
6. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.leftPacket_differential line 49
7. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.leftPacketComplex_eq line 98
8. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.rightPacketComplex_eq line 107