OAI/Topology/ArtinGroups/Functors/PacketSwitchMatrix.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.packetSwitchMatrixline 18 - lemma
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.switch_evaluationline 25 - def
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.packetComparisonline 55 - lemma
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.packetEvaluation_right_entryline 81 - lemma
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.packetEvaluation_left_entryline 92 - lemma
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.packetEvaluation_comparisonline 108