OAI/Topology/ArtinGroups/Complexes/HomInternalSupport.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homInternalSupportline 11 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.mem_homInternalSupportline 17 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homInternalSupport_dualline 26 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homSpace_off_internal_supportline 43 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homDimension_off_internal_supportline 61 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.totalHomDimensionline 73 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.totalChainDimensionline 77 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.totalHomDimension_dualline 81