OAI/Topology/ArtinGroups/Functors/PathSwitchEquiv.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.pathSwitchEquivline 14 - def
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.leftSectorsline 32 - def
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.rightSectorsline 51 - def
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearSwitchline 70 - lemma
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearSwitch_sectorline 82