OAI/Topology/ArtinGroups/Functors/ComplexPureLayer.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.HarmonicArtin.ReversibleQuiver.Iso.complex_pureLayerline 21 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Iso.classMap_layerline 26 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Iso.classMap_socleDimensionline 35 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Iso.classMap_topDimensionline 45 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Iso.levelArray_complexline 56 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Iso.classMap_levelArrayline 68