OAI/Topology/ArtinGroups/Complexes/HomDimensionDual.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classHomDimension_dualline 11 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeHomDimension_generatorArrayline 19 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeClassHomDimension_generatorArrayline 30 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeWordPerm_appendline 41 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeSignedPerm_inverseline 47 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeWordPerm_inverseline 51 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.probeOrbit_generator_dualline 60