OAI/Topology/ArtinGroups/Functors/HomSwitchMap.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.homSwitch_degreeline 17 - lemma
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.homUnswitch_degreeline 38 - def
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.homSwitchMapline 68 - def
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.homUnswitchMapline 82 - def
OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.homComparisonline 96