OAI/Topology/ArtinGroups/Complexes/FiniteSum2.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.finiteSum_entriesline 15 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.finiteSum_degreeline 31 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomotopyEquivalence.finiteSumline 44 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.sumTwistEquivline 80 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.sumTwist_eqline 92