OAI/Topology/ArtinGroups/Complexes/Sum.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classSumline 13 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classSum_mkline 19 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classSum_complexline 30 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classPositiveTwist_sumline 35 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classNegativeTwist_sumline 48