OAI/Topology/ArtinGroups/Complexes/PositiveTwistModern.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomotopyEquivalence.positiveTwistModern line 14
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveLayer_lowerTruncation line 21
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowPureIndex line 49
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowRestriction_bottom_eq_layer line 58
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classPositiveTwist_bottom_layer line 68
6. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveWord_bottom_layer line 82