OAI/Topology/ArtinGroups/Complexes/FiniteHomotopySetoid.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.finiteHomotopySetoid line 18
2. abbrev OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.FiniteHomotopyClass line 25
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classPositiveTwist line 27
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classNegativeTwist line 37
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classTwistPerm line 47
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classTwistPerm_orthogonal line 62
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classTwistPerm_adjacent line 72
8. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.FiniteModel.minimalRepresentative line 84
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.FiniteModel.minimalRepresentative_minimal line 88
10. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.FiniteModel.minimalRepresentativeEquivalence line 91
11. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classMultiplicity line 97
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classMultiplicity_of_minimal line 109