OAI/Topology/ArtinGroups/Complexes/MinimalModel.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.minimalClassModelline 12 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.minimalClassModel_minimalline 16 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.minimalClassModel_classline 21 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.minimalClassModel_homDimensionline 29 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.frameModelline 36 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.frameModel_minimalline 40 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.frameModel_linear_cycle_boundaryline 44 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.frameModel_orthogonal_cycle_boundaryline 60