OAI/Topology/ArtinGroups/Complexes/PositiveWord.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.FiniteModel.positiveWordline 13 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.FiniteModel.positiveWordMapline 17 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.FiniteModel.positiveWord_classline 22 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.FiniteModel.positiveWord_homMonoline 31 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomMonoFrom.compline 45 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomotopyEquivalence.homMonoFromline 57 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomMonoFrom.sourceEquivalenceline 70