OAI/Topology/ArtinGroups/Complexes/MinimalModelEquivalence.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.minimalClassModelEquivalenceline 17 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLayerline 21 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLayer_minimalline 26 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLayerSocleDimensionline 31 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLayerTopDimensionline 36 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLayerSocleDimension_minimalline 41 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLayerTopDimension_minimalline 49